no goals
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : A
M : Matrix n n A
⊢ invFun R A n (a • M) = a ⊗ₜ[R] 1 * invFun R A n M
simp [invFun, Finset.mul_sum]