English
If the index set is finite, then linear independence is characterized by the property that any two coefficient assignments yielding the same linear combination must be identical at every index.
Русский
Если множество индексов конечное, линейная независимость характеризуется тем, что любые две присвоения коэффициентов, дающие одинаковую линейную комбинацию, совпадают на каждом индексе.
LaTeX
$$$\\\\mathrm{LinearIndependent}_R(v) \\\\iff \\\\forall f,g : \\iota \\to R, \\\\Big( \\\\sum_i f(i) \\, v_i = \\\\sum_i g(i) \\, v_i \\\\Rightarrow \\\\forall i, f(i)=g(i) \\Big).$$$
Lean4
theorem linearIndependent_iffₛ [Fintype ι] :
LinearIndependent R v ↔ ∀ f g : ι → R, ∑ i, f i • v i = ∑ i, g i • v i → ∀ i, f i = g i := by
simp_rw [linearIndependent_iff_injective_fintypeLinearCombination, Injective, Fintype.linearCombination_apply,
funext_iff]
