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

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