English
For a finite index scenario, linear independence is equivalent to the injectivity of the map sending coefficient vectors to linear combinations; the zero relation implies all coefficients are zero.
Русский
Для конечного набора индексов линейная независимость эквивалентна инъективности отображения вектора коэффициентов в линейную комбинацию; нулевое соотношение implies все коэффициенты нули.
LaTeX
$$$$\\text{LI}_R(v) \\iff \\forall c:\\iota\\to R,\\; \\sum_{i} c(i) v(i)=0 \\Rightarrow c=0.$$$$
Lean4
theorem linearIndependent_iff_eq_zero_of_smul_mem_span :
LinearIndependent R v ↔ ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ { i })) → a = 0 :=
⟨fun hv ↦ hv.eq_zero_of_smul_mem_span, fun H =>
linearIndependent_iff.2 fun l hl => by
ext i; simp only [Finsupp.zero_apply]
by_contra hn
refine hn (H i _ ?_)
refine (Finsupp.mem_span_image_iff_linearCombination R).2 ⟨Finsupp.single i (l i) - l, ?_, ?_⟩
· rw [Finsupp.mem_supported']
intro j hj
have hij : j = i :=
Classical.not_not.1 fun hij : j ≠ i => hj ((mem_diff _).2 ⟨mem_univ _, fun h => hij (eq_of_mem_singleton h)⟩)
simp [hij]
· simp [hl]⟩
