Theorems · Definition · commutative algebra
Ring.choose
{R : Type u_1} → [inst : AddCommGroupWithOne R] → [inst_1 : Pow R ℕ] → [BinomialRing R] → R → ℕ → RThe binomial coefficient choose r n generalizes the natural number Nat.choose function,
interpreted in terms of choosing without replacement.
- Defined in
- Mathlib.RingTheory.Binomial
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
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.
- AddCommGroupWithOnestatement and proof · cited by 61
- BinomialRingstatement and proof · cited by 46
- Ring.multichooseproof · cited by 25
Cited by47
Results whose statement or proof uses this declaration.
- binomialSeriesproof · cited by 11
- PowerSeries.binomialSeriesproof · cited by 10
- LaurentSeries.hasseDerivproof · cited by 9
- Ring.descPochhammer_eq_factorial_smul_choosestatement · cited by 8
- mahlerproof · cited by 7
- Ring.choose_zero_right'statement · cited by 7
- PowerSeries.binomialSeries_coeffstatement and proof · cited by 7
- Ring.choose_natCaststatement · cited by 4
- HahnSeries.SummableFamily.binomialFamily_applystatement and proof · cited by 3
- Ring.choose_negstatement and proof · cited by 3
- Complex.one_add_cpow_hasFPowerSeriesOnBall_zeroproof · cited by 3
- binomialSeries_eq_ordinaryHypergeometricSeriesproof · cited by 2