Theorems · Definition · combinatorics

Multiset.foldr

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

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

Defined in

Mathlib.Data.Multiset.MapFold

Cited by

18 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext

Assumes

LeftCommutative