toLin'_mul — Mathlib

English

The linear map associated to the product of two matrices equals the composition of the linear maps associated to the factors.

Русский

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

LaTeX

$$$ \\mathrm{toLin'}(M N) = \\mathrm{toLin'}(M) \\circ \\mathrm{toLin'}(N) $$$

Lean4

@[simp]
theorem toLin'_mul [Fintype m] [DecidableEq m] (M : Matrix l m R) (N : Matrix m n R) :
    Matrix.toLin' (M * N) = (Matrix.toLin' M).comp (Matrix.toLin' N) :=
  Matrix.mulVecLin_mul _ _

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