English
For natural numbers n and k, (descPochhammer R k).eval(n) equals n descended factorial of k, cast to R.
Русский
Для натуральных n и k значение (descPochhammer R k) при n равно n-descFactorial(k) в кольце R.
LaTeX
$$$(\operatorname{descPochhammer}_R(k)).eval(n) = n^{\downarrow k}$$$
Lean4
theorem descPochhammer_eval_eq_descFactorial (n k : ℕ) : (descPochhammer R k).eval (n : R) = n.descFactorial k := by
induction k with
| zero => rw [descPochhammer_zero, eval_one, Nat.descFactorial_zero, Nat.cast_one]
| succ k
ih =>
rw [descPochhammer_succ_right, Nat.descFactorial_succ, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm k,
eval_natCast_mul, ← Nat.cast_comm n, ← sub_mul, ih]
by_cases h : n < k
· rw [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, mul_zero, mul_zero, Nat.cast_zero]
· rw [Nat.cast_mul, Nat.cast_sub <| not_lt.mp h]
