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 : ℕ
⊢ (1 / a) ^ n = 1 / a ^ n
simp only [one_div, inv_pow]