no goals
l : Type ?u.13040
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A ⬝ ⅟B ⬝ B = A
rw [Matrix.mul_assoc, Matrix.invOf_mul_self, Matrix.mul_one]