English
Let R be a commutative semiring and M1 a finite free R‑module with basis v1. The multiplicativity of the matrix representation is preserved for products of endomorphisms: the matrix of f*g equals the product of the matrices of f and g.
Русский
Пусть R — коммутативная полупрямая полугруппа, и M1 — конечнопорождаемый свободный R‑модуль с базисом v1. Произведение эндоморфизмов сохраняется на уровне матриц: матрица f g равна произведению матриц f и g.
LaTeX
$$$\operatorname{toMatrixAlgEquiv}_{v_1}(f \cdot g) = \operatorname{toMatrixAlgEquiv}_{v_1}(f) \cdot \operatorname{toMatrixAlgEquiv}_{v_1}(g).$$$
Lean4
theorem toMatrixAlgEquiv_mul (f g : M₁ →ₗ[R] M₁) :
LinearMap.toMatrixAlgEquiv v₁ (f * g) = LinearMap.toMatrixAlgEquiv v₁ f * LinearMap.toMatrixAlgEquiv v₁ g := by
rw [Module.End.mul_eq_comp, LinearMap.toMatrixAlgEquiv_comp v₁ f g]
