toMatrix'_mul — Mathlib

English

The matrix of the product of two endomorphisms equals the product of their matrices.

Русский

Матрица произведения эндоморфизмов равна произведению их матриц.

LaTeX

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

Lean4

theorem toMatrix'_mul [Fintype m] [DecidableEq m] (f g : (m → R) →ₗ[R] m → R) :
    LinearMap.toMatrix' (f * g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g :=
  LinearMap.toMatrix'_comp f g

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