English
For natural numbers n,m, the product of the descPochhammer polynomials satisfies: descPochhammer R n · (descPochhammer R m) ∘ (X − n) = descPochhammer R (n+m).
Русский
Для натуральных n,m произведение descPochhammer удовлетворяет: descPochhammer R n · (descPochhammer R m) ∘ (X − n) = descPochhammer R (n+m).
LaTeX
$$$\operatorname{descPochhammer}_R(n) \;\cdot\; (\operatorname{descPochhammer}_R(m))\circ (X - n) = \operatorname{descPochhammer}_R(n+m)$$$
Lean4
theorem descPochhammer_mul (n m : ℕ) :
descPochhammer R n * (descPochhammer R m).comp (X - (n : R[X])) = descPochhammer R (n + m) := by
induction m with
| zero => simp
| succ m ih =>
rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih, ← add_assoc,
descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]
