vecMul_injective_iff — Mathlib

English

For a matrix M, vecMul is injective if and only if the rows of M are linearly independent.

Русский

Для матрицы M отображение vecMul инъективно тогда и только тогда, когда строки M линейно независимы.

LaTeX

$$Function.Injective M.vecMul ↔ LinearIndependent R M.row$$

Lean4

theorem vecMul_injective_iff {M : Matrix m n R} : Function.Injective M.vecMul ↔ LinearIndependent R M.row :=
  by
  rw [← coe_vecMulLinear, linearIndependent_iff_injective_fintypeLinearCombination]
  congr! 1
  exact funext fun _ => Matrix.vecMul_eq_sum _ _

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