Theorems · Theorem · combinatorics

Multiset.fold_hom

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

Defined in

Mathlib.Data.Multiset.Fold

Cited by

1 results in Mathlib

Foundations

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

Assumes

Std.CommutativeStd.AssociativeStd.CommutativeStd.Associative