no goals
l : Type ?u.240416
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ det A⁻¹ * det A = 1
rw [← det_mul, A.nonsing_inv_mul h, det_one]