mulVecLin_zero — Mathlib

English

For any Fintype n, the matrix consisting of all zeros yields the zero linear map under mulVecLin.

Русский

Для любого конечного множества n матрица, состоящая только из нулей, обнуляет линейное отображение mulVecLin.

LaTeX

$$$\\forall [Fintype n],\\; \\text{Matrix.mulVecLin} (0 : \\text{Matrix } m\\, n\\, R) = 0$$$

Lean4

@[simp]
theorem mulVecLin_zero [Fintype n] : Matrix.mulVecLin (0 : Matrix m n R) = 0 :=
  LinearMap.ext zero_mulVec

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