English
For any ring R, the following identity holds: (descPochhammer R (n+1)).comp (X−1) = descPochhammer R (n+1) − (n+1)·(descPochhammer R n).comp (X−1).
Русский
Для кольца R имеет место: (descPochhammer R (n+1)).comp (X−1) = descPochhammer R (n+1) − (n+1)·(descPochhammer R n).comp (X−1).
LaTeX
$$$\big(\operatorname{descPochhammer}_R(n+1)\big)\circ (X-1) = \operatorname{descPochhammer}_R(n+1) - (n+1) \cdot (\operatorname{descPochhammer}_R(n))\circ (X-1)$$$
Lean4
theorem descPochhammer_succ_comp_X_sub_one (n : ℕ) :
(descPochhammer R (n + 1)).comp (X - 1) =
descPochhammer R (n + 1) - (n + (1 : R[X])) • (descPochhammer R n).comp (X - 1) :=
by
suffices
(descPochhammer ℤ (n + 1)).comp (X - 1) = descPochhammer ℤ (n + 1) - (n + 1) * (descPochhammer ℤ n).comp (X - 1) by
simpa [map_comp] using congr_arg (Polynomial.map (Int.castRingHom R)) this
nth_rw 2 [descPochhammer_succ_left]
rw [← sub_mul, descPochhammer_succ_right ℤ n, mul_comp, mul_comm, sub_comp, X_comp, natCast_comp]
ring
