Theorems · Theorem · combinatorics

Finset.fold_hom

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op]
  {f : α → β} {b : β} {s : Finset α} {op' : γ → γ → γ} [inst : Std.Commutative op'] [inst_1 : Std.Associative op']
  {m : β → γ},
  (∀ (x y : β), m (op x y) = op' (m x) (m y)) → Finset.fold op' (m b) (fun x => m (f x)) s = m (Finset.fold op b f s)

Defined in

Mathlib.Data.Finset.Fold

Cited by

0 results in Mathlib

Foundations

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

Assumes

Std.CommutativeStd.AssociativeStd.CommutativeStd.Associative