instAdd — Mathlib

English

The truncated Witt vectors form a ring with addition defined by truncating the sum 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 : Add (TruncatedWittVector p n R) :=
  ⟨fun x y => truncateFun n (x.out + y.out)⟩

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