instOne — Mathlib

English

The multiplicative identity in the truncated Witt vectors is given by truncating the Witt vector 1: 1 = truncateFun(n, 1).

Русский

Единица умножения в обрезанных виттовых векторах задаётся усечением виттового вектора 1: 1 = truncateFun(n, 1).

LaTeX

$$$ 1_{\mathrm{TruncatedWittVector}(p,n,R)} = \mathrm{truncateFun}(n)(1) $$$

Lean4

instance : One (TruncatedWittVector p n R) :=
  ⟨truncateFun n 1⟩

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