English
The truncated Witt vectors form a commutative ring; for each p, n, and a commutative ring R with p prime, TruncatedWittVector p n R carries a natural commutative ring structure induced from Witt vectors.
Русский
Усечённые виттовы вектора образуют коммутативное кольцо; для каждого p, n и кольца R с простым p имеется естественная структура кольца на TruncatedWittVector p n R, полученная из виттов via усечение.
LaTeX
$$$$\\mathrm{TruncatedWittVector}_{p}^{\,n}R \\text{ carries a commutative ring structure}. $$$$
Lean4
instance instCommRing : CommRing (TruncatedWittVector p n R) :=
(truncateFun_surjective p n R).commRing _ (truncateFun_zero p n R) (truncateFun_one p n R) (truncateFun_add n)
(truncateFun_mul n) (truncateFun_neg n) (truncateFun_sub n) (truncateFun_nsmul n) (truncateFun_zsmul n)
(truncateFun_pow n) (truncateFun_natCast n) (truncateFun_intCast n)
