ascPochhammer — Mathlib

English

For a semiring S and a natural number n, ascPochhammer S n is the polynomial X(X+1)···(X+n−1) (with ascPochhammer S 0 = 1).

Русский

Для полупрямого кольца S и натурального числа n многочлен ascPochhammer S n равен X(X+1)···(X+n−1) (при n=0 имеем ascPochhammer S 0 = 1).

LaTeX

$$$ascPochhammer(S,n) = \\prod_{i=0}^{n-1} (X+i)$ (с условием $ascPochhammer(S,0)=1$)$$

Lean4

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

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