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