toMatrixAlgEquiv'_comp — Mathlib

English

The matrix of a composition of linear maps equals the product of their matrices under the corresponding equivalence.

Русский

Матрица композиции линейных отображений равна произведению их матриц под соответствующим эквивалентством.

LaTeX

$$$ \\mathrm{toMatrixAlgEquiv'}(f \\circ g) = \\mathrm{toMatrixAlgEquiv'}(f) \\cdot \\mathrm{toMatrixAlgEquiv'}(g) $$$

Lean4

theorem toMatrixAlgEquiv'_comp (f g : (n → R) →ₗ[R] n → R) :
    LinearMap.toMatrixAlgEquiv' (f.comp g) = LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g :=
  LinearMap.toMatrix'_comp _ _

Похожие утверждения