English
An indexed set of vectors is linearly independent on a finite support if and only if the kernel of Finsupp.linearCombinationOn is trivial.
Русский
Индексированное множество векторов линейно независимо на конечной поддержке тогда и только тогда, когда ядро Finsupp.linearCombinationOn тривиально.
LaTeX
$$$$\\operatorname{LinearIndepOn}_R(v,s) \\iff \\ker\\big(\\mathrm{Finsupp.linearCombinationOn}\\;\\iota\\;M\\;R\\;v\\;s\\big) = \\bot.$$$$
Lean4
/-- An indexed set of vectors is linearly dependent iff there is a nontrivial
`Finsupp.linearCombination` of the vectors that is zero. -/
theorem linearDepOn_iff' :
¬LinearIndepOn R v s ↔ ∃ f : ι →₀ R, f ∈ Finsupp.supported R R s ∧ Finsupp.linearCombination R v f = 0 ∧ f ≠ 0 := by
simp [linearIndepOn_iff]
