ker_mulVecLin_eq_bot_iff — Mathlib

English

The kernel of mulVecLin is trivial if and only if every vector mapped to zero by M.mulVecLin is the zero vector.

Русский

Канал mulVecLin тривиален тогда и только тогда, когда из M.mulVecLin(v)=0 следует v=0.

LaTeX

$${M : Matrix m n R} : (LinearMap.ker M.mulVecLin) = ⊥ ↔ ∀ v, M *ᵥ v = 0 → v = 0$$

Lean4

theorem ker_mulVecLin_eq_bot_iff {M : Matrix m n R} : (LinearMap.ker M.mulVecLin) = ⊥ ↔ ∀ v, M *ᵥ v = 0 → v = 0 := by
  simp only [Submodule.eq_bot_iff, LinearMap.mem_ker, Matrix.mulVecLin_apply]

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