no goals
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a b : α
n : ℕ
⊢ 1 ^ ↑n = 1
rw [zpow_ofNat, one_pow]
no goals
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : DivisionMonoid α
a b : α
n : ℕ
⊢ 1 ^ Int.negSucc n = 1
rw [zpow_negSucc, one_pow, inv_one]