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

State before:
R : Type u_1
R' : Type u_2
inst✝² : AddMonoid R
inst✝¹ : CharTwo R
inst✝ : AddMonoid R'
φ : R' →+ R
h : Function.Injective ⇑φ
x : R'
⊢ φ (x + x) = φ 0
Tactic:
rw [φ.map_add, φ.map_zero, CharTwo.add_self_eq_zero]
State after:
no goals