English
For any v: ι → M, LinearIndepOn R v s is equivalent to the kernel of Finsupp.linearCombination R v restricted to coefficients supported in s being trivial; i.e., ker(Finsupp.linearCombination R v) intersected with the allowed support is {0}.
Русский
Для v: ι → M линейная независимость на s эквивалентна тому, что ядро линейной комбинации ограничено опорой в s тривиально.
LaTeX
$$$$\\operatorname{LinearIndepOn}_R(v,s) \\iff \\ker\\big(\\mathrm{Finsupp.linearCombination}\\,R\\,v\\big) \\;\\perp\\; \\text{??? bottom condition ???}$$$$
Lean4
/-- If the kernel of a linear map is disjoint from the span of a family of vectors,
then the family is linearly independent iff it is linearly independent after composing with
the linear map. -/
protected theorem linearIndependent_iff_of_disjoint (f : M →ₗ[R] M')
(hf_inj : Disjoint (span R (Set.range v)) (LinearMap.ker f)) :
LinearIndependent R (f ∘ v) ↔ LinearIndependent R v :=
f.linearIndependent_iff_of_injOn <| LinearMap.injOn_of_disjoint_ker le_rfl hf_inj
