no goals
l : Type ?u.293786
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
k : αˣ
h : IsUnit (det A)
⊢ (k⁻¹ • A⁻¹) ⬝ (k • A) = 1
simp [h, smul_smul]