English
For linear maps f: M2→M3 and g: M1→M2, the matrix of the composition f∘g with respect to bases v1,v3 equals the product of the matrices of f and g with appropriate bases: toMatrix v1 v3 (f ∘ g) = toMatrix v2 v3 f · toMatrix v1 v2 g.
Русский
Пусть f: M2→M3 и g: M1→M2 — линейные отображения. Матрица композиции f∘g по базисам v1,v3 равна произведению матриц: toMatrix v1 v3 (f ∘ g) = toMatrix v2 v3 f · toMatrix v1 v2 g.
LaTeX
$$$\mathrm{toMatrix}_{v_1,v_3}(f \circ g) = \mathrm{toMatrix}_{v_2,v_3}(f) \; \mathrm{toMatrix}_{v_1,v_2}(g)$$$
Lean4
theorem toMatrix_comp [Finite l] [DecidableEq m] (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂) :
LinearMap.toMatrix v₁ v₃ (f.comp g) = LinearMap.toMatrix v₂ v₃ f * LinearMap.toMatrix v₁ v₂ g :=
by
simp_rw [LinearMap.toMatrix, LinearEquiv.trans_apply]
rw [LinearEquiv.arrowCongr_comp _ v₂.equivFun, LinearMap.toMatrix'_comp]
