Theorems · Theorem · combinatorics

Multiset.bell_mul_eq

∀ (m : Multiset ℕ),
  m.bell * (Multiset.map (fun j => j.factorial) m).prod * ∏ j ∈ m.toFinset.erase 0, (Multiset.count j m).factorial =
    m.sum.factorial

Defined in

Mathlib.Combinatorics.Enumerative.Bell

Cited by

2 results in Mathlib

Foundations

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