mulVecLin_add — Mathlib

English

For any matrices M, N, the linear map associated to M + N equals the sum of the linear maps associated to M and to N.

Русский

Для любых матриц M и N линейное отображение, соответствующее M + N, равно сумме отображений, соответствующих M и N.

LaTeX

$$$ (M + N).mulVecLin = M.mulVecLin + N.mulVecLin $$$

Lean4

@[simp]
theorem mulVecLin_add [Fintype n] (M N : Matrix m n R) : (M + N).mulVecLin = M.mulVecLin + N.mulVecLin :=
  LinearMap.ext fun _ ↦ add_mulVec _ _ _

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