English
If the index set ι is finite, then LinearIndependent R v is equivalent to the statement that the only coefficient function g: ι → R with ∑ i g(i) v(i) = 0 is the zero function.
Русский
Если множество индексов ι конечное, то LinearIndependent R v эквивалентно тому, что единственная функция коэффициентов g: ι → R с ∑ i g(i) v(i) = 0 равна нулю.
LaTeX
$$$$\\operatorname{LinearIndependent}_R(v) \\iff \\forall g:\\iota \\to R,\\; \\Big(\\sum_{i} g(i)\\,v(i) = 0 \\Rightarrow \\forall i,\\; g(i)=0\\Big).$$$$
Lean4
theorem linearIndependent_iff [Fintype ι] : LinearIndependent R v ↔ ∀ g : ι → R, ∑ i, g i • v i = 0 → ∀ i, g i = 0 :=
by
refine
⟨fun H g => by simpa using linearIndependent_iff'.1 H Finset.univ g, fun H =>
linearIndependent_iff''.2 fun s g hg hs i => H _ ?_ _⟩
rw [← hs]
refine (Finset.sum_subset (Finset.subset_univ _) fun i _ hi => ?_).symm
rw [hg i hi, zero_smul]
