mulRightLinearMap_eq_zero_iff — Mathlib

English

For a matrix a, mulRightLinearMap l R a = 0 iff a = 0 (with suitable nonempty index assumptions).

Русский

Правое умножение на матрицу A даёт нулевое отображение тогда и только тогда, когда A = 0.

LaTeX

$$$\operatorname{mulRightLinearMap}\ l\ R\ a = 0 \;\iff\; a = 0$$$

Lean4

/-- A version of `LinearMap.mulRight_eq_zero_iff` for matrix multiplication. -/
@[simp]
theorem mulRightLinearMap_eq_zero_iff (a : Matrix m n A) [Nonempty l] : mulRightLinearMap l R a = 0 ↔ a = 0 :=
  by
  constructor <;> intro h
  · inhabit l
    ext i j
    classical
    replace h := DFunLike.congr_fun h (Matrix.single (default : l) i 1)
    simpa using Matrix.ext_iff.2 h default j
  · rw [h]
    exact mulRightLinearMap_zero_eq_zero _ _

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