Theorems · Definition · combinatorics

Finset.fold

{α : Type u_1} →
  {β : Type u_2} → (op : β → β → β) → [hc : Std.Commutative op] → [ha : Std.Associative op] → β → (α → β) → Finset α → β

fold op b f s folds the commutative associative operation op over the f-image of s, i.e. fold (+) b f {1,2,3} = f 1 + f 2 + f 3 + b.

Defined in

Mathlib.Data.Finset.Fold

Cited by

46 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

Std.CommutativeStd.Associative