Theorem: IMOSL.Extra.CharTwo.ofRingHom (IMOSLLean4/Extra/CharTwo/Ring/Hom.lean)

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CharTwo R
inst✝ : NonAssocSemiring S
φ : R →+* S
⊢ 2 = 0
Tactic:
rw [← one_add_one_eq_two, ← φ.map_one,
← φ.map_add, add_self_eq_zero, φ.map_zero]
State after:
no goals