linearIndependent_iff — Mathlib

English

Let v: ι → M be a family of vectors in a module over R. The family is linearly independent over R if and only if the only coefficient function l: ι → R with Finsupp.linearCombination R v l = 0 is the zero function l = 0.

Русский

Пусть v : ι → M—семейство векторов над R. Семейство линейно независимо тогда и только тогда, когда единственная функция коэффициентов l : ι → R с Finsupp.linearCombination R v l = 0 есть нулевая функция.

LaTeX

$$$$\\operatorname{LinearIndependent}_R(v) \\iff \\forall l,\\; Finsupp.linearCombination R v\\, l = 0 \\rightarrow l = 0.$$$$

Lean4

theorem linearIndependent_iff : LinearIndependent R v ↔ ∀ l, Finsupp.linearCombination R v l = 0 → l = 0 := by
  simp [linearIndependent_iff_ker, LinearMap.ker_eq_bot']

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