toMatrixAlgEquiv'_mul — Mathlib

English

The map f ↦ toMatrixAlgEquiv'(f) preserves multiplication of linear maps.

Русский

Умножение линейных отображений сохраняется под преобразованием toMatrixAlgEquiv'.

LaTeX

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

Lean4

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

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