out — Mathlib

English

Given a truncated Witt vector x, we can embed it into Witt vectors by setting all higher coefficients to zero.

Русский

Дан усечённый Witt-вектор x, его можно рассмотреть как Witt-вектор, заполнив нулями все последующие коэффициенты.

LaTeX

$$$\\mathrm{out}\\ x = \\mathrm{WittVector.mk'}\\ p\\ (\\lambda i. \\text{if } i < n \\text{ then } x.coeff \\ i \\text{ else } 0)$$$

Lean4

/-- We can turn a truncated Witt vector `x` into a Witt vector
by setting all coefficients after `x` to be 0.
-/
def out (x : TruncatedWittVector p n R) : 𝕎 R :=
  @WittVector.mk' p _ fun i => if h : i < n then x.coeff ⟨i, h⟩ else 0

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