no goals
R : Type u_3
inst✝⁴ : CommSemiring R
k : Type ?u.691401
l : Type u_2
m : Type u_1
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix l m R
N : Matrix m n R
x : n → R
⊢ ↑(↑toLin' (M ⬝ N)) x = ↑(↑toLin' M) (↑(↑toLin' N) x)
rw [Matrix.toLin'_mul, LinearMap.comp_apply]