no goals
l : Type ?u.99734
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)
⊢ A⁻¹ = 0
rw [inv_def, Ring.inverse_non_unit _ h, zero_smul]