no goals
R : Type u_3
inst✝¹¹ : CommSemiring R
l : Type u_1
m : Type u_2
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_6
M₂ : Type u_7
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_5
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
x : M₁
⊢ ↑(↑(toLin v₁ v₃) (A ⬝ B)) x = ↑(↑(toLin v₂ v₃) A) (↑(↑(toLin v₁ v₂) B) x)
rw [Matrix.toLin_mul v₁ v₂, LinearMap.comp_apply]