English
There is a ring homomorphism truncate n: 𝕎 R → TruncatedWittVector p n R that sends a Witt vector to its first n components.
Русский
Существует гомоморфизм кольца truncate n: 𝕎 R → TruncatedWittVector p n R, который отправляет виттовектор в его первые n координат.
LaTeX
$$$$\\operatorname{truncate}_n: \\mathbb{W}R \\to+* \\mathrm{TruncatedWittVector}_{p}^{\,n}R \\text{ is a ring homomorphism}. $$$$
Lean4
/-- `truncate n` is a ring homomorphism that truncates `x` to its first `n` entries
to obtain a `TruncatedWittVector`, which has the same base `p` as `x`. -/
noncomputable def truncate : 𝕎 R →+* TruncatedWittVector p n R
where
toFun := truncateFun n
map_zero' := truncateFun_zero p n R
map_add' := truncateFun_add n
map_one' := truncateFun_one p n R
map_mul' := truncateFun_mul n
