toMatrix_mul — Mathlib

English

For linear maps f,g: M1→M1, the matrix of the product fg with respect to a basis equals the product of the matrices of f and g: toMatrix v1 v1 (f g) = toMatrix v1 v1 f · toMatrix v1 v1 g.

Русский

Для линейных отображений f,g: M1→M1 матрица произведения fg по базису равна произведению матриц: toMatrix v1 v1 (f g) = toMatrix v1 v1 f · toMatrix v1 v1 g.

LaTeX

$$$\mathrm{toMatrix}_{v_1,v_1}(f \circ g) = \mathrm{toMatrix}_{v_1,v_1}(f) \cdot \mathrm{toMatrix}_{v_1,v_1}(g)$$$

Lean4

theorem toMatrix_mul (f g : M₁ →ₗ[R] M₁) :
    LinearMap.toMatrix v₁ v₁ (f * g) = LinearMap.toMatrix v₁ v₁ f * LinearMap.toMatrix v₁ v₁ g := by
  rw [Module.End.mul_eq_comp, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]

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