English
A refinement of the Finset form: if two coefficient functions coincide outside a Finset, independence implies equality of the coefficients on that Finset.
Русский
Уточнение в виде Finset: если две функции коэффициентов совпадают вне Finset, независимость влечёт равенство коэффициентов внутри Finset.
LaTeX
$$$\\operatorname{LinearIndependent}(R,v) \\iff \\forall s:\\operatorname{Finset} ι, \\forall f,g:ι→R, (\\forall i\\notin s, f_i=g_i) \\Rightarrow (\\sum_{i\\in s} f_i v_i = \\sum_{i\\in s} g_i v_i \\Rightarrow \\forall i\\in s, f_i=g_i)$$$
Lean4
/-- A subfamily of a linearly independent family (i.e., a composition with an injective map) is a
linearly independent family. -/
theorem comp (h : LinearIndependent R v) (f : ι' → ι) (hf : Injective f) : LinearIndependent R (v ∘ f) := by
simpa [comp_def] using Injective.comp h (Finsupp.mapDomain_injective hf)
