wittAdd — Mathlib

English

The polynomials governing addition in 𝕎R are given by wittAdd p = wittStructureInt p (X0 + X1).

Русский

Полиномы, задающие сложение в 𝕎R: wittAdd p = wittStructureInt p (X0 + X1).

LaTeX

$$$\\mathrm{WittVector.wittAdd}(p) = wittStructureInt(p, X_0 + X_1)$$$

Lean4

/-- The polynomials used for defining the addition of the ring of Witt vectors. -/
def wittAdd : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ :=
  wittStructureInt p (X 0 + X 1)

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