descPochhammer — Mathlib

English

For a ring R, the descending Pochhammer polynomial descPochhammer R n is the product X, (X−1), …, (X−n+1) in R[X].

Русский

Для кольца R descendPochhammer R n есть произведение X, (X−1), …, (X−n+1) в кольце R[X].

LaTeX

$$$\operatorname{descPochhammer}_R(n) = X \cdot (X-1) \cdot \dots \bigl(X-(n-1)\bigr)$$$

Lean4

/-- `descPochhammer R n` is the polynomial `X * (X - 1) * ... * (X - n + 1)`,
with coefficients in the ring `R`.
-/
noncomputable def descPochhammer : ℕ → R[X]
  | 0 => 1
  | n + 1 => X * (descPochhammer n).comp (X - 1)

Похожие утверждения