English
If the family is not linearly independent, there exist two coefficient functions witnessing a nontrivial relation, i.e., there is a finite sum with equal linear combinations but different coefficients at some index.
Русский
Если семейство латинно не линейно независимо, существуют две функции коэффициентов, дающие одну и ту же линейную комбинацию, но различающиеся на каком-либо индексе.
LaTeX
$$$\\\\neg \\\\mathrm{LinearIndependent}_R(v) \\\\iff \\\\exists f,g : \iota \\to R, \\\\Big( \\\\sum_i f(i) \\, v_i = \\\\sum_i g(i) \\, v_i \\\\land \\\\exists i, f(i) \neq g(i) \Big).$$$
Lean4
theorem not_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
simpa using not_iff_not.2 Fintype.linearIndependent_iffₛ