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 : α
⊢ a⁻¹ ^ 0 = (a ^ 0)⁻¹
rw [pow_zero, pow_zero, inv_one]
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 + 1) = (a ^ (n + 1))⁻¹
rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]