no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℤ
⊢ A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹
rw [mul_assoc, mul_eq_mul A, mul_nonsing_inv _ h, mul_one]
no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℤ
⊢ A ^ (n - 1) * A * A⁻¹ = A ^ n * A⁻¹
rw [← zpow_add_one h, sub_add_cancel]