instCommRing — Mathlib

English

ghostComponent(n) evaluates the n-th Witt polynomial on the first n coefficients of x.

Русский

ghostComponent(n) вычисляет n-ую полином Витта на первых n коэффициентах x.

LaTeX

$$$\\mathrm{ghostComponent}(n) = (\\text{the } n\text{-th Witt polynomial})\\text{ evaluated at } x.\\text{coeff}_{1..n}$$$

Lean4

/-- The commutative ring structure on `𝕎 R`. -/
instance : CommRing (𝕎 R) :=
  (mapFun.surjective _ <| counit_surjective _).commRing (mapFun <| MvPolynomial.counit _) (mapFun.zero _) (mapFun.one _)
    (mapFun.add _) (mapFun.mul _) (mapFun.neg _) (mapFun.sub _) (mapFun.nsmul _) (mapFun.zsmul _) (mapFun.pow _)
    (mapFun.natCast _) (mapFun.intCast _)

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