Theorems · Definition · combinatorics

Multiset.foldl

{α : Type u_1} → {β : Type v} → (f : β → α → β) → [RightCommutative f] → β → Multiset α → β

foldl f H b s is the lift of the list operation foldl f b l, which folds f over the multiset. It is well defined when f is right-commutative, that is, f (f b a₁) a₂ = f (f b a₂) a₁.

Defined in

Mathlib.Data.Multiset.MapFold

Cited by

13 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

RightCommutative