instMul — Mathlib

English

For a prime p and a commutative ring R, the Witt vectors 𝕎_p(R) form a ring with multiplication defined through Witt polynomials: x · y = eval (wittMul p) (![x, y]).

Русский

Для простого p и коммутативного кольца R Witt-вектора 𝕎_p(R) образуют кольцо; умножение задаётся через полиномы Witt: x · y = eval (wittMul p) (![x, y]).

LaTeX

$$$$ x \cdot y = \mathrm{eval}\big(\mathrm{wittMul}(p)\big)(![x, y]). $$$$

Lean4

instance : Mul (𝕎 R) :=
  ⟨fun x y => eval (wittMul p) ![x, y]⟩

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