Theorems · Theorem · combinatorics

Multiset.card_pi

∀ {α : Type u_1} [inst : DecidableEq α] {β : α → Type u_2} (m : Multiset α) (t : (a : α) → Multiset (β a)),
  (m.pi t).card = (Multiset.map (fun a => (t a).card) m).prod

Defined in

Mathlib.Data.Multiset.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEq