frobenius_isPoly — Mathlib

English

Frobenius is a tautological polynomial function on Witt vectors: frobenius is a polynomial map in the Witt coordinates.

Русский

Frobenius на Witt-векторах является тождественно полиномиальным отображением по координатам Witt.

LaTeX

$$$\text{frobenius isPoly} \; \;\text{on Witt vectors}.$$$

Lean4

/-- `frobenius` is tautologically a polynomial function. -/
instance frobenius_isPoly : IsPoly p fun R _Rcr => @frobenius p R _ _Rcr :=
  frobeniusFun_isPoly _

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