English
For matrices A ∈ Mat_{l×m}(R) and B ∈ Mat_{m×n}(R), the corresponding linear maps satisfy: Matrix.toLin v1 v3 (A B) = (Matrix.toLin v2 v3 A) ∘ (Matrix.toLin v1 v2 B).
Русский
Для матриц A и B размерности l×m и m×n над R соответствующие линейные отображения удовлетворяют: Matrix.toLin v1 v3 (A B) = (Matrix.toLin v2 v3 A) ∘ (Matrix.toLin v1 v2 B).
LaTeX
$$$\mathrm{toLin}_{v_1,v_3}(A B) = \big(\mathrm{toLin}_{v_2,v_3}(A)\big) \circ \big(\mathrm{toLin}_{v_1,v_2}(B)\big)$$$
Lean4
theorem toLin_mul [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) :
Matrix.toLin v₁ v₃ (A * B) = (Matrix.toLin v₂ v₃ A).comp (Matrix.toLin v₁ v₂ B) :=
by
apply (LinearMap.toMatrix v₁ v₃).injective
haveI : DecidableEq l := fun _ _ ↦ Classical.propDecidable _
rw [LinearMap.toMatrix_comp v₁ v₂ v₃]
repeat' rw [LinearMap.toMatrix_toLin]
