Theorems · Theorem · commutative algebra
descPochhammer_succ_right
∀ (R : Type u) [inst : Ring R] (n : ℕ), descPochhammer R (n + 1) = descPochhammer R n * (Polynomial.X - ↑n)
- Defined in
- Mathlib.RingTheory.Polynomial.Pochhammer
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites29
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringproof · cited by 13,802
- RingHomproof · cited by 10,189
- Ringstatement and proof · cited by 7,463
- Polynomialstatement and proof · cited by 5,681
- Algebra.algebraMapproof · cited by 4,706
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- Nat.cast_oneproof · cited by 2,501
- mul_assocproof · cited by 1,667
- Polynomial.Xstatement and proof · cited by 1,639
- sub_zeroproof · cited by 938
- Polynomial.mapproof · cited by 806
Cited by14
Results whose statement or proof uses this declaration.
- descPochhammer_eval_eq_descFactorialproof · cited by 3
- descPochhammer_succ_evalproof · cited by 3
- Complex.one_add_cpow_hasFPowerSeriesOnBall_zeroproof · cited by 3
- Polynomial.descPochhammer_smeval_eq_ascPochhammerproof · cited by 2
- descPochhammer_eval_eq_prod_rangeproof · cited by 2
- Polynomial.ascPochhammer_smeval_neg_eq_descPochhammerproof · cited by 1
- descPochhammer_eq_ascPochhammerproof · cited by 1
- Polynomial.descPochhammer_smeval_eq_descFactorialproof · cited by 1
- Ring.descPochhammer_smeval_addproof · cited by 1
- Ring.descPochhammer_succ_succ_smevalproof · cited by 1
- descPochhammer_mulproof · cited by 1
- descPochhammer_natDegreeproof · cited by 1