mulVec_injective_iff — Mathlib

English

The map v ↦ M.mulVec v is injective if and only if the columns of M are linearly independent.

Русский

Отображение v ↦ M.mulVec v инъективно тогда и только тогда, когда столбцы матрицы независимы линейно.

LaTeX

$${M : Matrix m n R} : Function.Injective M.mulVec ↔ LinearIndependent R M.col$$

Lean4

theorem mulVec_injective_iff {M : Matrix m n R} : Function.Injective M.mulVec ↔ LinearIndependent R M.col :=
  by
  change Function.Injective (fun x ↦ _) ↔ _
  simp_rw [← M.vecMul_transpose, vecMul_injective_iff, row_transpose]

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