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 : α
h : Commute a b
n : ℕ
⊢ (a * b) ^ ↑n = a ^ ↑n * b ^ ↑n
simp [zpow_ofNat, h.mul_pow n]
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 : α
h : Commute a b
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n
simp [h.mul_pow, (h.pow_pow _ _).eq, mul_inv_rev]