toLin'_mul_apply — Mathlib

English

For matrices M, N and vector x, the vector obtained by applying the product corresponds to applying the left factor after applying the right factor to x.

Русский

Для матриц M, N и вектора x применение произведения отображает результат: сначала применяем N к x, затем M к результату.

LaTeX

$$$ \\mathrm{toLin'}(M N) \\, x = \\mathrm{toLin'}(M)\\bigl(\\mathrm{toLin'}(N)\\, x\\bigr)$$$

Lean4

/-- Shortcut lemma for `Matrix.toLin'_mul` and `LinearMap.comp_apply` -/
theorem toLin'_mul_apply [Fintype m] [DecidableEq m] (M : Matrix l m R) (N : Matrix m n R) (x) :
    Matrix.toLin' (M * N) x = Matrix.toLin' M (Matrix.toLin' N x) := by rw [Matrix.toLin'_mul, LinearMap.comp_apply]

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