no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
n : ℕ
⊢ (A * B) ^ ↑n = A ^ ↑n * B ^ ↑n
simp [h.mul_pow n, -mul_eq_mul]
no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
n : ℕ
⊢ (A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]
rw [zpow_negSucc, zpow_negSucc, zpow_negSucc, mul_eq_mul _⁻¹, ← mul_inv_rev, ← mul_eq_mul,
  h.mul_pow n.succ, (h.pow_pow _ _).eq]