English
For any v, s, and the map Finsupp.linearCombinationOn ι M R v s, LinearIndepOn v s is equivalent to ker of this linear map being bottom.
Русский
Для v, s и отображения Finsupp.linearCombinationOn линейная независимость на s эквивалентна тому, что ядро отображения равно нижнему подпростению.
LaTeX
$$$$\\operatorname{LinearIndepOn}_R(v,s) \\iff \\big( \\ker\\big(\\mathrm{Finsupp.linearCombinationOn}\\;\\iota\\;M\\;R\\;v\\;s\\big) = \\bot \\big).$$$$
Lean4
theorem linearIndepOn_iff :
LinearIndepOn R v s ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0 :=
linearIndepOn_iffₛ.trans
⟨fun h l hl ↦ h l hl 0 (zero_mem _), fun h f hf g hg eq ↦
sub_eq_zero.mp (h (f - g) (sub_mem hf hg) <| by rw [map_sub, eq, sub_self])⟩
