verschiebungPoly — Mathlib

English

The Verschiebung polynomial at n is 0 if n = 0, and otherwise is the Witt polynomial variable X(n−1).

Русский

Полйном Verschiebung(n) равен 0 при n = 0, иначе X(n−1).

LaTeX

$$$$ verschiebungPoly(n) = \\begin{cases}0, & n=0 \\\\ X(n-1), & n>0.\\end{cases} $$$$

Lean4

/-- The 0th Verschiebung polynomial is 0. For `n > 0`, the `n`th Verschiebung polynomial is the
variable `X (n-1)`.
-/
def verschiebungPoly (n : ℕ) : MvPolynomial ℕ ℤ :=
  if n = 0 then 0 else X (n - 1)

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