The rising factorial as a product #
ascPochhammer_eval_eq_prod_range: (ascPochhammer R n).eval r = r (r + 1) ⋯ (r + n - 1), the
rising-factorial counterpart of mathlib's descPochhammer_eval_eq_prod_range.
[UPSTREAM] candidate for Mathlib.RingTheory.Polynomial.Pochhammer.
theorem
ascPochhammer_eval_eq_prod_range
{R : Type u_1}
[CommSemiring R]
(n : ℕ)
(r : R)
:
Polynomial.eval r (ascPochhammer R n) = ∏ j ∈ Finset.range n, (r + ↑j)