Theorems · Definition · commutative algebra
ascPochhammer
(S : Type u) → [inst : Semiring S] → ℕ → Polynomial S
ascPochhammer S n is the polynomial X * (X + 1) * ... * (X + n - 1),
with coefficients in the semiring S.
- Defined in
- Mathlib.RingTheory.Polynomial.Pochhammer
- Cited by
- 80 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Polynomialstatement · cited by 5,681
Cited by88
Results whose statement or proof uses this declaration.
- Ring.factorial_nsmul_multichoose_eq_ascPochhammerstatement · cited by 12
- ascPochhammer_succ_leftstatement and proof · cited by 11
- ascPochhammer_succ_rightstatement and proof · cited by 11
- Polynomial.preHilbertPolyproof · cited by 11
- Complex.regularizedHGFunCoeffproof · cited by 10
- Ring.descPochhammer_eq_factorial_smul_chooseproof · cited by 8
- ordinaryHypergeometricCoefficientproof · cited by 7
- ascPochhammer_nat_eq_ascFactorialstatement · cited by 6
- ascPochhammer_mapstatement and proof · cited by 5
- descPochhammer_eval_eq_ascPochhammerstatement and proof · cited by 4
- ascPochhammer_eval_caststatement and proof · cited by 4
- Polynomial.ascPochhammer_smeval_caststatement and proof · cited by 3