mulVecLin_mul — Mathlib

English

For matrices M and N, the mulVecLin of the product equals the composition of mulVecLin with mulVecLin.

Русский

Для матриц M и N выполняется: mulVecLin(M N) = (mulVecLin M) ∘ (mulVecLin N).

LaTeX

$$Matrix.mulVecLin (M * N) = (Matrix.mulVecLin M).comp (Matrix.mulVecLin N)$$

Lean4

@[simp]
theorem mulVecLin_mul [Fintype m] (M : Matrix l m R) (N : Matrix m n R) :
    Matrix.mulVecLin (M * N) = (Matrix.mulVecLin M).comp (Matrix.mulVecLin N) :=
  LinearMap.ext fun _ ↦ (mulVec_mulVec _ _ _).symm

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