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

State before:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : CharTwo R
inst✝ : NoZeroDivisors R
x : R
⊢ x ^ 2 = 1 ↔ x = 1
Tactic:
rw [sq, mul_self_eq_one_iff]
State after:
no goals