English
The right-branch recurrence: ascPochhammer S (n+1) = ascPochhammer S n · (X + n).
Русский
Правое следование: ascPochhammer S (n+1) = ascPochhammer S n · (X + n).
LaTeX
$$$ascPochhammer S (n+1) = ascPochammer S n \\cdot (X + n)$$$
Lean4
theorem ascPochhammer_succ_right (n : ℕ) : ascPochhammer S (n + 1) = ascPochhammer S n * (X + (n : S[X])) :=
by
suffices h : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + (n : ℕ[X]))
by
apply_fun Polynomial.map (algebraMap ℕ S) at h
simpa only [ascPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X, Polynomial.map_natCast] using h
induction n with
| zero => simp
| succ n ih =>
conv_lhs =>
rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp, X_comp, natCast_comp,
add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]
