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 * A
simp only [← Nat.cast_succ, pow_succ', zpow_ofNat]
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) + 1) = (A ^ n)⁻¹
rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_ofNat]
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)⁻¹ = (A ⬝ A ^ n)⁻¹ ⬝ A
rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.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 ⬝ A ^ n)⁻¹ ⬝ A = A ^ (-(↑n + 1)) * A
rw [zpow_neg h, ← Int.ofNat_succ, zpow_ofNat, pow_succ, mul_eq_mul, mul_eq_mul]