no goals
l : Type ?u.252005
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
⊢ IsUnit (det A⁻¹) ↔ IsUnit (det A)
rw [Matrix.det_nonsing_inv, isUnit_ring_inverse]