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✝ : DivisionCommMonoid α
a b : α
n : ℤ
⊢ (a / b) ^ n = a ^ n / b ^ n
simp only [div_eq_mul_inv, mul_zpow, inv_zpow]