R✝ : Type ?u.400
inst✝³ : AddMonoidWithOne R✝
inst✝² : CharZero R✝
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
q n : ℕ
hn : n ≠ 0
⊢ q ^ n = 1 ↔ q = 1
R✝ : Type ?u.400
inst✝³ : AddMonoidWithOne R✝
inst✝² : CharZero R✝
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
q n : ℕ
hn : n ≠ 0
⊢ ↑q ^ n = 1 ↔ q = 1
rw [← cast_pow, cast_eq_one]
no goals
R✝ : Type ?u.400
inst✝³ : AddMonoidWithOne R✝
inst✝² : CharZero R✝
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
q n : ℕ
hn : n ≠ 0
⊢ q ^ n = 1 ↔ q = 1
exact pow_eq_one_iff hn