English
Let v: ι → M be a family of vectors in a module M over R. Then v is linearly independent over R if and only if the only finitely supported linear combination that equals 0 is the trivial one; equivalently the kernel of the linear combination map Finsupp.linearCombination R v is the zero submodule.
Русский
Пусть v : ι → M — семейство векторов в модуле M над кольцом R. Тогда {v_i} линейно независимо по R тогда и только тогда, когда единственная линейная комбинация с конечной опорой, равная нулю, тривиальна; эквивалентно ядро отображения линейной комбинации по v равно нулевому подпространению.
LaTeX
$$$$\\operatorname{LinearIndependent}_R(v) \\iff \\ker\\big(\\mathrm{Finsupp.linearCombination}\\,R\\,v\\big) = \\bot.$$$$
Lean4
theorem linearIndependent_iff_ker : LinearIndependent R v ↔ LinearMap.ker (Finsupp.linearCombination R v) = ⊥ :=
LinearMap.ker_eq_bot.symm
