_example — Mathlib

English

The Verschiebung map is a polynomial function in Witt coordinates.

Русский

Переход Verschiebung является полиномиальной функцией Witt-координат.

LaTeX

$$$$ \\mathrm{verschiebung} : 𝕎R \\to 𝕎R \\text{ is a polynomial map; } \\mathrm{verschiebung}(x) = \\text{(polynomial in } x) . $$$$

Lean4

example (p : ℕ) (f : ⦃R : Type _⦄ → [CommRing R] → WittVector p R → WittVector p R) [IsPoly p f] :
    IsPoly p (fun (R : Type*) (I : CommRing R) ↦ verschiebungFun ∘ (@f R I)) :=
  inferInstance

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