Theorems · Theorem · combinatorics

Multiset.count_bind

∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α},
  Multiset.count a (m.bind f) = (Multiset.map (fun b => Multiset.count a (f b)) m).sum

Defined in

Mathlib.Data.Multiset.Bind

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEq