Theorems · Theorem · combinatorics
Nat.multinomial_two_mul_le_mul_multinomial
∀ {ι : Type u_1} {s : Finset ι} {f : ι → ℕ},
(Nat.multinomial s fun i => 2 * f i) ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * Nat.multinomial s f- Defined in
- Mathlib.Data.Nat.Choose.Multinomial
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 61 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.
- Finsetstatement and proof · cited by 13,712
- Finset.sumstatement and proof · cited by 5,195
- Finset.prodproof · cited by 2,356
- le_reflproof · cited by 2,061
- le_of_ltproof · cited by 1,175
- ne_of_gtproof · cited by 637
- Nat.factorialproof · cited by 616
- mul_posproof · cited by 374
- pow_posproof · cited by 292
- mul_le_mul'proof · cited by 274
- mul_powproof · cited by 220
- Finset.mul_sumproof · cited by 196
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.