English
For a matrix a, the left-multiplication map by a is the zero map iff a = 0 (under appropriate finiteness and scalar-tower assumptions).
Русский
Левое умножение на матрицу A даёт нулевое отображение тогда и только тогда, когда A = 0 (при надлежащих предположениях о конечности и отношении скалярных действий).
LaTeX
$$$\operatorname{mulLeftLinearMap}\ n\ R\ a = 0 \;\iff\; a = 0$$$
Lean4
/-- A version of `LinearMap.mulLeft_eq_zero_iff` for matrix multiplication. -/
@[simp]
theorem mulLeftLinearMap_eq_zero_iff [Nonempty n] (a : Matrix l m A) : mulLeftLinearMap n R a = 0 ↔ a = 0 :=
by
constructor <;> intro h
· inhabit n
ext i j
classical
replace h := DFunLike.congr_fun h (Matrix.single j (default : n) 1)
simpa using Matrix.ext_iff.2 h i default
· rw [h]
exact mulLeftLinearMap_zero_eq_zero _ _
