instNeg — Mathlib

English

Negation on truncated Witt vectors is defined by truncating the negation of the underlying Witt vector: -x = truncateFun(n)(-x.out).

Русский

Отрицание обрезанных виттовых векторов задаётся как усечение отрицания исходного виттового вектора: -x = truncateFun(n)(-x.out).

LaTeX

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

Lean4

instance : Neg (TruncatedWittVector p n R) :=
  ⟨fun x => truncateFun n (-x.out)⟩

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