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 : α
m n : ℤ
⊢ a ^ (m * n) = (a ^ n) ^ m
rw [mul_comm, zpow_mul]