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 a : α
n : ℕ
⊢ a⁻¹ ^ ↑n = (a ^ ↑n)⁻¹
rw [zpow_ofNat, zpow_ofNat, inv_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 a : α
n : ℕ
⊢ a⁻¹ ^ Int.negSucc n = (a ^ Int.negSucc n)⁻¹
rw [zpow_negSucc, zpow_negSucc, inv_pow]