Theorem: IMOSL.IMO2012A5.𝔽₂ε.castRingHom_injective (IMOSLLean4/IMO2012/A5/Extra/ExplicitRings/F2e.lean)

State before:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharTwo R
r : R
h : r * r = 0
h0 : r ≠ 0
h1 : 1 = 0
⊢ r = 0
Tactic:
rw [← one_mul r, h1, zero_mul]
State after:
no goals

State before:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharTwo R
r : R
h : r * r = 0
h0 : r ≠ 0
h1 : 1 ≠ 0
x : 𝔽₂ε
h2 : (castRingHom h) Y = 0
⊢ 1 = 0
Tactic:
rwa [add_eq_zero_iff_eq.mp h2, one_mul] at h
State after:
no goals