Theorems · Definition · combinatorics
Nat.multinomial
{α : Type u_1} → Finset α → (α → ℕ) → ℕThe multinomial coefficient. Gives the number of strings consisting of symbols
from s, where c ∈ s appears with multiplicity f c.
Defined as (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!.
- Defined in
- Mathlib.Data.Nat.Choose.Multinomial
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Finset.sumproof · cited by 5,195
- Finset.prodproof · cited by 2,356
- Nat.factorialproof · cited by 616
Cited by35
Results whose statement or proof uses this declaration.
- Nat.multinomial_emptystatement · cited by 6
- Multiset.bellproof · cited by 6
- Nat.uniformBell_eqproof · cited by 5
- Nat.multinomial_insertstatement and proof · cited by 4
- Nat.multinomial_specstatement · cited by 4
- Nat.binomial_eq_choosestatement · cited by 3
- Nat.multinomial_consstatement and proof · cited by 3
- Finsupp.multinomial_updateproof · cited by 2
- Nat.multinomial_congrstatement · cited by 2
- Nat.multinomial_singletonstatement and proof · cited by 2
- Multiset.bell_mul_eqproof · cited by 2
- Finsupp.multinomial_eq_of_support_subsetstatement · cited by 1