addIsPoly₂ — Mathlib

English

Addition of Witt vectors is a polynomial function in the Witt coordinates.

Русский

Сложение векторов Witt задаётся полиномиальной функцией по координатам Witt.

LaTeX

$$$\exists F_i \in \mathbb{Z}[X_j]_{j\le i} \quad \text{such that } (F_0(w_1,w_2), F_1(w_1,w_2), \dots) = w_1 + w_2$ for all Witt vectors $w_1,w_2$.$$

Lean4

/-- Addition of Witt vectors is a polynomial function. -/
instance addIsPoly₂ [Fact p.Prime] : IsPoly₂ p fun _ _ => (· + ·) :=
  ⟨⟨wittAdd p, by intros; ext; exact add_coeff _ _ _⟩⟩

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