English
For finite index ι, LinearIndependent R v is equivalent to the injectivity of the map sending coefficient vector to the corresponding linear combination, equivalently the map c ↦ ∑ i c(i) v(i) is injective.
Русский
Для конечного индекса ι линейная независимость эквивалентна инъективности отображения коэффициентов в их линейную комбинацию.
LaTeX
$$$$\\operatorname{LinearIndependent}_R(v) \\iff \\text{Injective}\\left(c\\mapsto \\sum_{i} c(i) v(i)\\right).$$$$
Lean4
/-- A finite family of vectors `v i` is linear independent iff the linear map that sends
`c : ι → R` to `∑ i, c i • v i` is injective. -/
theorem linearIndependent_iff'ₛ [Fintype ι] [DecidableEq ι] :
LinearIndependent R v ↔ Injective (LinearMap.lsum R (fun _ ↦ R) ℕ fun i ↦ LinearMap.id.smulRight (v i)) := by
simp [Fintype.linearIndependent_iffₛ, Injective, funext_iff]
