English
For all n, descPochhammer R (n+1) equals descPochhammer R n multiplied by (X − n).
Русский
Для любого n: descPochhammer R (n+1) = descPochhammer R n · (X − n).
LaTeX
$$$\operatorname{descPochhammer}_R(n+1) = \operatorname{descPochhammer}_R(n) \cdot (X - n)$$$
Lean4
theorem descPochhammer_succ_right (n : ℕ) : descPochhammer R (n + 1) = descPochhammer R n * (X - (n : R[X])) :=
by
suffices h : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - (n : ℤ[X]))
by
apply_fun Polynomial.map (algebraMap ℤ R) at h
simpa [descPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X, Polynomial.map_intCast] using h
induction n with
| zero => simp [descPochhammer]
| succ n
ih =>
conv_lhs =>
rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp, X_comp,
natCast_comp]
rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]
