English
Define truncateFun(n, x) as the truncated Witt vector formed by the first n coefficients of x; i.e., it keeps the first n components of x.
Русский
Определяем отображение усечения, которое берет у виттового вектора x первые n коэффициентов и формирует усечённый виттов вектор.
LaTeX
$$$ (\mathrm{truncateFun}(n)(x)).\mathrm{coeff} i = x.\mathrm{coeff} i \quad \text{for all } i : \mathrm{Fin}(n) $$$
Lean4
/-- `truncateFun n x` uses the first `n` entries of `x` to construct a `TruncatedWittVector`,
which has the same base `p` as `x`.
This function is bundled into a ring homomorphism in `WittVector.truncate` -/
def truncateFun (x : 𝕎 R) : TruncatedWittVector p n R :=
TruncatedWittVector.mk p fun i => x.coeff i
