English
The smeval of the descPochhammer with integer index k evaluated at r equals the smeval of the ascPochhammer with natural index k evaluated at r−k+1, linking desc and asc forms.
Русский
Значение smeval(descPochhammer ℤ k) при аргументе r равно smeval(ascPochhammer ℕ k) при аргументе r−k+1.
LaTeX
$$$(\mathrm{descPochhammer} \ℤ k).\mathrm{smeval}\; r = (\mathrm{ascPochhammer} \ℕ k).\mathrm{smeval}\; (r - k + 1)$$$
Lean4
theorem descPochhammer_smeval_eq_ascPochhammer (r : R) (n : ℕ) :
(descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - n + 1) := by
induction n with
| zero => simp only [descPochhammer_zero, ascPochhammer_zero, smeval_one, npow_zero]
| succ n
ih =>
rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right, smeval_mul, ih,
ascPochhammer_succ_left, X_mul, smeval_mul_X, smeval_comp, smeval_sub, ← C_eq_natCast, smeval_add, smeval_one,
smeval_C]
simp only [smeval_X, npow_one, npow_zero, zsmul_one, Int.cast_natCast, one_smul]
