Theorem: IMOSL.Extra.CharTwo.mul_self_eq_one_iff (IMOSLLean4/Extra/CharTwo/Ring/Basic.lean)

State before:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : CharTwo R
inst✝ : NoZeroDivisors R
x : R
⊢ x * x = 1 ↔ x = 1
Tactic:
rw [← add_eq_zero_iff_eq, ← add_one_mul_self, mul_self_eq_zero, add_eq_zero_iff_eq]
State after:
no goals