no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
A : M
h : IsUnit (det A)
⊢ A ^ (-n) * A ^ n = 1
rw [zpow_neg h, mul_eq_mul, nonsing_inv_mul _ (h.det_zpow _)]