English
The integer-descended Pochhammer equals the ascPochhammer composed with a linear shift: descPochhammer ℤ n = (ascPochhammer ℤ n) ∘ ((X) − n + 1).
Русский
DescPochhammer ℤ n равен ascPochhammer ℤ n, сопоставленной через композицию с линейным сдвигом: descPochhammer ℤ n = (ascPochhammer ℤ n) ∘ (X − n + 1).
LaTeX
$$$\operatorname{descPochhammer}_\mathbb{Z} n = (\operatorname{ascPochhammer}_\mathbb{Z} n) \circ (X - n + 1)$$$
Lean4
theorem descPochhammer_eval_eq_ascPochhammer (r : R) (n : ℕ) :
(descPochhammer R n).eval r = (ascPochhammer R n).eval (r - n + 1) := by
induction n with
| zero => rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
| succ n ih =>
rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih, ascPochhammer_succ_left, X_mul,
eval_mul_X,
show (X + 1 : R[X]) = (X + 1 : ℕ[X]).map (algebraMap ℕ R) by
simp only [Polynomial.map_add, map_X, Polynomial.map_one],
ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
