English
There is a relation between the descPochhammer smeval and the descFactorial: smeval of (descPochhammer ℤ k) at n equals n.descFactorial k (cast appropriately).
Русский
Связь smeval(descPochhammer) и descFactorial: smeval(descPochhammer ℤ k) в n равен n.descFactorial k (с соответствующим отображением типов).
LaTeX
$$$\big(\mathrm{descPochhammer} \ℤ k\big).\mathrm{smeval}\; (n) = n.descFactorial\; k$$$
Lean4
theorem descPochhammer_smeval_eq_descFactorial (n k : ℕ) : (descPochhammer ℤ k).smeval (n : R) = n.descFactorial k := by
induction k with
| zero => rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]
| succ k
ih =>
rw [descPochhammer_succ_right, Nat.descFactorial_succ, smeval_mul, ih, mul_comm, Nat.cast_mul, smeval_sub, smeval_X,
smeval_natCast, npow_one, npow_zero, nsmul_one]
by_cases h : n < k
· simp only [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, zero_mul]
· rw [Nat.cast_sub <| not_lt.mp h]
