Theorem: IMOSL.Extra.CharTwo.sq_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 ^ 2 = y ^ 2 ↔ x = y
Tactic:
rw [sq, sq, mul_self_eq_iff]
State after:
no goals