mulRightLinearMap_zero_eq_zero — Mathlib

English

The right-linear map sends the zero matrix to the zero linear map, i.e., mulRightLinearMap l R (0 : Matrix m n A) = 0.

Русский

Правая линейная карта отображает нулевую матрицу в нулевую линейную карту: mulRightLinearMap l R (0 : Matrix m n A) = 0.

LaTeX

$$$$mulRightLinearMap\\ l\\ R\\ (0) = 0.$$$$

Lean4

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

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