α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u * u = 1 ↔ u = 1 ∨ u = -1
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u⁻¹ = u ↔ u = 1 ∨ u = -1
rw [inv_eq_iff_mul_eq_one]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑(u * u) = ↑1 ↔ ↑u = ↑1 ∨ ↑u = ↑(-1)
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u * u = 1 ↔ u = 1 ∨ u = -1
simp only [ext_iff]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑u * ↑u = 1 ↔ ↑u = 1 ∨ ↑u = -1
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑(u * u) = ↑1 ↔ ↑u = ↑1 ∨ ↑u = ↑(-1)
push_cast
no goals
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑u * ↑u = 1 ↔ ↑u = 1 ∨ ↑u = -1
exact mul_self_eq_one_iff