English
For r in a semiring and k in N, smeval of ascPochhammer ℕ (k+1) at r+1 satisfies a recurrence: smeval(ascPochhammer ℕ (k+1)) (r+1) = factorial(k+1) · multichoose (r+1) k + smeval(ascPochhammer ℕ (k+1)) r.
Русский
Для r из полупрямоугольного кольца и k∈ℕ выполняется рециррентная формула для smeval ascPochhammer ℕ (k+1) в точке r+1.
LaTeX
$$$\mathrm{smeval}(\mathrm{ascPochhammer}\\mathbb{N} (k+1))(r+1) = k! \,?$$$
Lean4
theorem ascPochhammer_succ_succ (r : R) (k : ℕ) :
smeval (ascPochhammer ℕ (k + 1)) (r + 1) =
Nat.factorial (k + 1) • multichoose (r + 1) k + smeval (ascPochhammer ℕ (k + 1)) r :=
by
nth_rw 1 [ascPochhammer_succ_right, ascPochhammer_succ_left, mul_comm (ascPochhammer ℕ k)]
simp only [smeval_mul, smeval_comp, smeval_add, smeval_X]
rw [Nat.factorial, mul_smul, factorial_nsmul_multichoose_eq_ascPochhammer]
simp only [smeval_one, npow_one, npow_zero, one_smul]
rw [← C_eq_natCast, smeval_C, npow_zero, add_assoc, add_mul, add_comm 1, @nsmul_one, add_mul]
rw [← @nsmul_eq_mul, @add_rotate', @succ_nsmul, add_assoc]
simp_all only [Nat.cast_id, nsmul_eq_mul, one_mul]
