English
Let v: ι → M be a family of vectors. The family is linearly independent over R if and only if for every finite subset s of ι and every function g: ι → R, the condition ∑ i∈s g(i) v(i) = 0 implies g(i) = 0 for all i ∈ s.
Русский
Пусть v : ι → M. Семейство линейно независимо по R тогда и только тогда, когда для любой конечной подмножества s ⊆ ι и любой функции g: ι → R из условия ∑ i∈s g(i) v(i) = 0 следует g(i) = 0 для всех i ∈ s.
LaTeX
$$$$\\operatorname{LinearIndependent}_R(v) \\iff \\forall s : \\mathrm{Finset}\\,\\iota, \\ \\forall g : \\iota \\to R, \\ \\Big(\\sum_{i\\in s} g(i) \\cdot v(i) = 0 \\Rightarrow \\forall i \\in s,\\; g(i) = 0\\Big).$$$$
Lean4
/-- A version of `linearIndependent_iff` where the linear combination is a `Finset` sum. -/
theorem linearIndependent_iff' :
LinearIndependent R v ↔ ∀ s : Finset ι, ∀ g : ι → R, ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0 :=
by
rw [linearIndependent_iff'ₛ]
refine ⟨fun h s f ↦ ?_, fun h s f g ↦ ?_⟩
· convert h s f 0; simp_rw [Pi.zero_apply, zero_smul, Finset.sum_const_zero]
· rw [← sub_eq_zero, ← Finset.sum_sub_distrib]
convert h s (f - g) using 3 <;> simp only [Pi.sub_apply, sub_smul, sub_eq_zero]
