English
Viewing a module as the affine space modeled on itself, a weighted vector subtraction is just a linear combination. Precisely, for a finite set s, weights w: s → k, and p: s → V with the sum of weights zero, the weightedVSub equals the ordinary linear combination ∑_{i∈s} w(i) p(i).
Русский
Представляя модуль как аффинное пространство над самим собой, взвешенная векторная разность равна линейной комбинации: если s—конечное множество, w: s → k, p: s → V и сумма w равна нулю, то s.weightedVSub p w = ∑_{i∈s} w(i) p(i).
LaTeX
$$$$\sum_{i\in s} w(i) \cdot p(i) = s.weightedVSub p w\quad\text{whenever}\quad \sum_{i\in s} w(i)=0.$$$$
Lean4
/-- Viewing a module as an affine space modelled on itself, a `weightedVSub` is just a linear
combination. -/
@[simp]
theorem weightedVSub_eq_linear_combination {ι} (s : Finset ι) {w : ι → k} {p : ι → V} (hw : s.sum w = 0) :
s.weightedVSub p w = ∑ i ∈ s, w i • p i := by
simp [s.weightedVSub_apply, vsub_eq_sub, smul_sub, ← Finset.sum_smul, hw]
