Theorems · Definition · commutative algebra
Ring.multichoose
{R : Type u_1} → [inst : AddCommMonoid R] → [inst_1 : Pow R ℕ] → [BinomialRing R] → R → ℕ → RThe multichoose function is the quotient of ascending Pochhammer evaluation by the corresponding
factorial. When applied to natural numbers, multichoose k n describes choosing a multiset of n
items from a type of size k, i.e., choosing with replacement.
- Defined in
- Mathlib.RingTheory.Binomial
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- AddCommMonoidPowBinomialRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommMonoidstatement and proof · cited by 12,281
- BinomialRingstatement and proof · cited by 46
- BinomialRing.multichooseproof · cited by 2
Cited by26
Results whose statement or proof uses this declaration.
- Ring.chooseproof · cited by 43
- Ring.factorial_nsmul_multichoose_eq_ascPochhammerstatement · cited by 12
- Ring.choose_zero_right'proof · cited by 7
- Ring.multichoose_one_right'statement · cited by 2
- Ring.multichoose_succ_succstatement and proof · cited by 2
- Ring.multichoose_zero_rightstatement · cited by 2
- Ring.multichoose_zero_right'statement · cited by 2
- Ring.map_chooseproof · cited by 1
- Ring.map_multichoosestatement and proof · cited by 1
- Ring.ascPochhammer_succ_succstatement and proof · cited by 1
- Ring.multichoose_eqstatement and proof · cited by 1
- Ring.multichoose_onestatement and proof · cited by 1