ghostComponent — Mathlib

English

The value ghostComponent(n)(x) equals the evaluation of the nth Witt polynomial at x.coeff.

Русский

Значение ghostComponent(n)(x) равно вычислению n-й полинома Витта по x.coeff.

LaTeX

$$$ ghostComponent(n)(x) = aeval\\,(x.\\coeff)\\,(W_{\\mathbb{Z}}(n))$$$

Lean4

/-- Evaluates the `n`th Witt polynomial on the first `n` coefficients of `x`,
producing a value in `R`. -/
def ghostComponent (n : ℕ) : 𝕎 R →+* R :=
  (Pi.evalRingHom _ n).comp ghostMap

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