mulIsPoly₂ — Mathlib

English

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

Русский

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

LaTeX

$$$\exists G_i \in \mathbb{Z}[X_j] \quad \text{such that } (G_0(w_1,w_2), G_1(w_1,w_2), \dots) = w_1 \cdot w_2$ for all Witt vectors $w_1,w_2$.$$

Lean4

/-- Multiplication of Witt vectors is a polynomial function. -/
instance mulIsPoly₂ [Fact p.Prime] : IsPoly₂ p fun _ _ => (· * ·) :=
  ⟨⟨wittMul p, by intros; ext; exact mul_coeff _ _ _⟩⟩
    -- unfortunately this is not universe polymorphic, merely because `f` isn't

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