Theorems · Theorem · combinatorics

Finset.fold_map

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op]
  {f : α → β} {b : β} {g : γ ↪ α} {s : Finset γ}, Finset.fold op b f (Finset.map g s) = Finset.fold op b (f ∘ ⇑g) s

Defined in

Mathlib.Data.Finset.Fold

Cited by

2 results in Mathlib

Foundations

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

Assumes

Std.CommutativeStd.Associative