instMul — Mathlib

English

The truncated Witt vectors form a ring with multiplication defined by truncating the product of the underlying Witt vectors: x * y = truncateFun(n)(x.out * y.out).

Русский

Обрезанные виттовы векторы образуют кольцо; умножение задается как усечение произведения соответствующих виттовых векторов: x * y = truncateFun(n)(x.out * y.out).

LaTeX

$$$ x * y = \mathrm{truncateFun}(n)(x.\mathrm{out} * y.\mathrm{out}) $$$

Lean4

instance : Mul (TruncatedWittVector p n R) :=
  ⟨fun x y => truncateFun n (x.out * y.out)⟩

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