wittZero — Mathlib

English

The polynomials defining the zero element of the Witt ring are given by wittZero p = wittStructureInt p 0.

Русский

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

LaTeX

$$$\\mathrm{WittVector.wittZero}(p) = wittStructureInt(p,0)$$$

Lean4

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

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