English
Let v be a linearly independent family in an R-module M. For any x in the index set and any finitely supported f: ι → R with x not in the support of f, the R-linear combination f.linearCombination v is not equal to v_x.
Русский
Пусть v — линейно независимая совокупность в модуле над R. Пусть x принадлежит ι, а f: ι → R имеет конечную опору и x не лежит в опоре f. Тогда линейная комбинация f линейно сочетаний по v не равна v_x.
LaTeX
$$$\\forall x\\in ι\\,\\forall f\\in ι\\to_{0}R:\\, x\\notin f\\mathrm{supp}\\,\\Rightarrow f\\cdot v\\;\\neq\\; v_x$$$
Lean4
theorem linearCombination_ne_of_notMem_support [Nontrivial R] (hv : LinearIndependent R v) {x : ι} (f : ι →₀ R)
(h : x ∉ f.support) : f.linearCombination R v ≠ v x :=
by
replace h : x ∉ (f.support : Set ι) := h
intro w
have p : ∀ x ∈ Finsupp.supported R R f.support, Finsupp.linearCombination R v x ≠ f.linearCombination R v := by
simpa [← w, Finsupp.span_image_eq_map_linearCombination] using hv.notMem_span_image h
exact p f (f.mem_supported_support R) rfl
