weightedVSub_smul — Mathlib

English

If you scale the underlying points by a scalar a in a group acting on the vector space, the weightedVSub scales accordingly.

Русский

Если основные точки масштабируются скалярной величиной a, взвешенная сумма VSub масштабируется пропорционально.

LaTeX

$$$\displaystyle s.weightedVSub (a\cdot p) w = a\cdot s.weightedVSub p w$$$

Lean4

theorem weightedVSub_smul {G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V] {s : Finset ι} {w : ι → k}
    (h : ∑ i ∈ s, w i = 0) (p : ι → V) (a : G) : s.weightedVSub (a • p) w = a • s.weightedVSub p w := by
  rw [weightedVSub, weightedVSubOfPoint_smul, weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]

Похожие утверждения