Theorems · Inductive type · commutative algebra
BinomialRing
(R : Type u_1) → [AddCommMonoid R] → [Pow R ℕ] → Type u_1
A binomial ring is a ring for which ascending Pochhammer evaluations are uniquely divisible by
suitable factorials. We define this notion as a mixin for additive commutative monoids with natural
number powers, but retain the ring name. We introduce Ring.multichoose as the uniquely defined
quotient.
- Defined in
- Mathlib.RingTheory.Binomial
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- AddCommMonoidPow
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommMonoidstatement · cited by 12,281
Cited by57
Results whose statement or proof uses this declaration.
- Ring.choosestatement and proof · cited by 43
- Ring.multichoosestatement and proof · cited by 25
- Ring.factorial_nsmul_multichoose_eq_ascPochhammerstatement and proof · cited by 12
- PowerSeries.binomialSeriesstatement and proof · cited by 10
- HahnSeries.SummableFamily.binomialFamilystatement and proof · cited by 8
- Ring.descPochhammer_eq_factorial_smul_choosestatement and proof · cited by 8
- Ring.choose_zero_right'statement and proof · cited by 7
- PowerSeries.binomialSeries_coeffstatement and proof · cited by 7
- Ring.choose_natCaststatement and proof · cited by 4
- HahnSeries.SummableFamily.binomialFamily_applystatement and proof · cited by 3
- Ring.choose_negstatement and proof · cited by 3
- HahnSeries.SummableFamily.orderTop_hsum_binomialFamily_posstatement and proof · cited by 3