English
A recurrence for smeval of descPochhammer: smeval (descPochhammer ℤ (k+1)) (r+1) equals (k+1) times smeval (descPochhammer ℤ k) r plus smeval (descPochhammer ℤ (k+1)) r.
Русский
Рекуррентное соотношение для smeval descPochhammer: smeval(descPochhammer ℤ (k+1)) (r+1) = (k+1)·smeval(descPochhammer ℤ k) r + smeval(descPochhammer ℤ (k+1)) r.
LaTeX
$$$ \forall R\ [NonAssocRing\ R]\ [Pow\ R\ ℕ]\ [NatPowAssoc\ R]\ (r: R)\ (k: \mathbb{N}),\ smeval(\descPochhammer\ ℤ (k+1))(r+1) = (k+1) \cdot smeval(\descPochhammer\ ℤ k) r + smeval(\descPochhammer\ ℤ (k+1)) r$$$
Lean4
theorem descPochhammer_succ_succ_smeval {R} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (r : R) (k : ℕ) :
smeval (descPochhammer ℤ (k + 1)) (r + 1) =
(k + 1) • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ (k + 1)) r :=
by
nth_rw 1 [descPochhammer_succ_left]
rw [descPochhammer_succ_right, mul_comm (descPochhammer ℤ k)]
simp only [smeval_comp, smeval_sub, smeval_mul, smeval_X, smeval_one, npow_one, npow_zero, one_smul,
add_sub_cancel_right, sub_mul, add_mul, add_smul, one_mul]
rw [← C_eq_natCast, smeval_C, npow_zero, add_comm (k • smeval (descPochhammer ℤ k) r) _, add_assoc,
add_comm (k • smeval (descPochhammer ℤ k) r) _, ← add_assoc, ← add_sub_assoc, nsmul_eq_mul, zsmul_one,
Int.cast_natCast, sub_add_cancel, add_comm]
