wittOne — Mathlib

English

The polynomials defining the unit element of the Witt ring are given by wittOne p = wittStructureInt p 1.

Русский

Для единичного Witt‑вектора используются полиномы wittOne p = wittStructureInt p 1.

LaTeX

$$$\\mathrm{WittVector.wittOne}(p) = wittStructureInt(p,1)$$$

Lean4

/-- The polynomials used for defining the element `1` of the ring of Witt vectors. -/
def wittOne : ℕ → MvPolynomial (Fin 0 × ℕ) ℤ :=
  wittStructureInt p 1

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