English
The descending Pochhammer with integer parameter n satisfies (descPochhammer ℤ n).smeval r = n! · choose r n. This links the smeval of descending pochhammer to the binomial coefficient via factorial.
Русский
Убывающий Похаммер с целочисленным параметром n удовлетворяет (descPochhammer ℤ n).smeval r = n! · choose r n, связывая smeval убывающего pochhammer с биномиальным коэффициентом через факториал.
LaTeX
$$$ \big(\descPochhammer\ \mathbb{Z}\ n\big).smeval\, r = n\,\text{factorial} \cdot \operatorname{choose} \; r\; n$$$
Lean4
theorem descPochhammer_eq_factorial_smul_choose [NatPowAssoc R] (r : R) (n : ℕ) :
(descPochhammer ℤ n).smeval r = n.factorial • choose r n :=
by
rw [choose, factorial_nsmul_multichoose_eq_ascPochhammer, descPochhammer_eq_ascPochhammer, smeval_comp, add_comm_sub,
smeval_add, smeval_X, npow_one]
have h : smeval (1 - n : Polynomial ℤ) r = 1 - n :=
by
rw [← C_eq_natCast, ← C_1, ← C_sub, smeval_C]
simp only [npow_zero, zsmul_one, Int.cast_sub, Int.cast_one, Int.cast_natCast]
rw [h, ascPochhammer_smeval_cast, add_comm_sub]
