∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
  {G : Type u_6} [inst_3 : Group G] [inst_4 : DistribMulAction G V] [SMulCommClass G k V] {s : Finset ι} {w : ι → k},
  ∑ i ∈ s, w i = 0 → ∀ (p : ι → V) (a : G), (s.weightedVSub (a • p)) w = a • (s.weightedVSub p) w