mulLeftLinearMap_zero_eq_zero — Mathlib

English

The left-linear map sends the zero matrix to the zero linear map, i.e., mulLeftLinearMap n R (0) = 0.

Русский

Левая линейная карта отправляет нулевую матрицу в нулевую линейную карту: mulLeftLinearMap n R (0) = 0.

LaTeX

$$$$mulLeftLinearMap\\ n\\ R\\ (0) = 0.$$$$

Lean4

/-- A version of `LinearMap.mulLeft_zero_eq_zero` for matrix multiplication. -/
@[simp]
theorem mulLeftLinearMap_zero_eq_zero : mulLeftLinearMap n R (0 : Matrix l m A) = 0 :=
  LinearMap.ext fun _ => Matrix.zero_mul _

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