Theorems · Theorem · combinatorics

Multiset.fold_bind

∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] {ι : Type u_4} (s : Multiset ι)
  (t : ι → Multiset α) (b : ι → α) (b₀ : α),
  Multiset.fold op (Multiset.fold op b₀ (Multiset.map b s)) (s.bind t) =
    Multiset.fold op b₀ (Multiset.map (fun i => Multiset.fold op (b i) (t i)) s)

Defined in

Mathlib.Data.Multiset.Bind

Cited by

1 results in Mathlib

Foundations

Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Std.CommutativeStd.Associative