Theorems · Theorem · combinatorics
Nat.uniformBell_mul_eq
∀ (m : ℕ) {n : ℕ}, n ≠ 0 → m.uniformBell n * n.factorial ^ m * m.factorial = (m * n).factorial- Defined in
- Mathlib.Combinatorics.Enumerative.Bell
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- Finset.prodproof · cited by 2,356
- Multiset.mapproof · cited by 876
- Finset.prod_congrproof · cited by 646
- Nat.factorialstatement and proof · cited by 616
- Multiset.prodproof · cited by 528
- Finset.eraseproof · cited by 455
- Multiset.sumproof · cited by 388
- Multiset.countproof · cited by 302
- Multiset.toFinsetproof · cited by 230
- Multiset.replicateproof · cited by 88
- Finset.prod_singletonproof · cited by 78
Cited by2
Results whose statement or proof uses this declaration.
- DividedPowers.OfInvertibleFactorial.dpow_comp_of_mul_ltproof · cited by 1
- Nat.uniformBell_eq_divproof · cited by 0