English
Let R be a commutative ring and n a nonnegative integer. Then the value of the descending Pochhammer polynomial descPochhammer at r equals the product of the linear factors (r − j) for j = 0,1,...,n−1; i.e., (descPochhammer R n).eval(r) = ∏_{j=0}^{n-1} (r − j).
Русский
Пусть R — равномерное кольцо (коммутативное кольцо), n — неотрицательное целое, и возьмем элемент r. Значение descended Pochhammer(descPochhammer) в r равно произведению (r − j) по j от 0 до n−1, т.е. (descPochhammer R n).eval(r) = ∏_{j=0}^{n−1} (r − j).
LaTeX
$$$(\\operatorname{descPochhammer} \\, R\\, n).\\mathrm{eval}\\, r = \\prod_{j=0}^{n-1} (r - j)$$$
Lean4
theorem descPochhammer_eval_eq_prod_range {R : Type*} [CommRing R] (n : ℕ) (r : R) :
(descPochhammer R n).eval r = ∏ j ∈ Finset.range n, (r - j) := by
induction n with
| zero => simp
| succ n ih => simp [descPochhammer_succ_right, ih, ← Finset.prod_range_succ]
