ker_toLin'_eq_bot_iff — Mathlib

English

The kernel of the matrix-to-linear-map correspondence is zero iff the matrix has trivial right kernel: M v = 0 implies v = 0 for all v.

Русский

Ядро отображения, переводящего матрицу в линейное отображение, равно нулю тогда и только тогда, когда для всех векторов v из n пространства M v = 0 влечёт v = 0.

LaTeX

$$$ \\ker\\bigl(\\mathrm{toLin'}(M)\\bigr) = \\{0\\} \\iff \\forall v,\\ M \\cdot v = 0 \\Rightarrow v = 0 $$$

Lean4

theorem ker_toLin'_eq_bot_iff {M : Matrix n n R} : LinearMap.ker (Matrix.toLin' M) = ⊥ ↔ ∀ v, M *ᵥ v = 0 → v = 0 :=
  Matrix.ker_mulVecLin_eq_bot_iff

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