weight — Mathlib

English

The weight of a finitely supported function f with respect to a weight function w is the additive combination of weights: weight w f = sum_i f(i) • w(i).

Русский

Вес функции с конечной опорой по весовой функции w определяется как сумма по i: f(i) • w(i).

LaTeX

$$weight w : (σ →₀ R) →+ M defined by weight w f = ∑ i, f i • w i$$

Lean4

/-- The `weight` of the finitely supported function `f : σ →₀ R`
with respect to `w : σ → M` is the sum `∑ i, f i • w i`. -/
noncomputable def weight : (σ →₀ R) →+ M :=
  (Finsupp.linearCombination R w).toAddMonoidHom

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