Theorems · Definition · commutative algebra

Finsupp.weight

{σ : Type u_1} →
  {M : Type u_2} →
    {R : Type u_3} → [inst : Semiring R] → (σ → M) → [inst_1 : AddCommMonoid M] → [Module R M] → (σ →₀ R) →+ M

The weight of the finitely supported function f : σ →₀ R with respect to w : σ → M is the sum ∑ i, f i • w i.

Defined in

Mathlib.Data.Finsupp.Weight

Cited by

90 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModule