weightedVSub_const_smul — Mathlib

English

A constant multiplier c can be pulled out of the weights: s.weightedVSub p (c • w) = c • s.weightedVSub p w.

Русский

Константный множитель можно вынести за пределы весов: s.weightedVSub p (c • w) = c • s.weightedVSub p w.

LaTeX

$$$ s.weightedVSub p (c \cdot w) = c \cdot s.weightedVSub p w $$$

Lean4

/-- A constant multiplier of the weights in `weightedVSub_of` may be moved outside the sum. -/
theorem weightedVSub_const_smul (w : ι → k) (p : ι → P) (c : k) : s.weightedVSub p (c • w) = c • s.weightedVSub p w :=
  s.weightedVSubOfPoint_const_smul _ _ _ _

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