frobenius_bijective — Mathlib

English

For a prime p and a ring R of characteristic p with the perfect ring property, the Frobenius endomorphism on Witt vectors p is bijective.

Русский

Для простого числа p и кольца R характеристикой p с свойством идеального кольца, отображение Фробениуса на Witt-векторах p является биективным.

LaTeX

$$$\operatorname{frobenius}: \mathrm{WittVector}_p(R) \to \mathrm{WittVector}_p(R)$ is bijective$$

Lean4

theorem frobenius_bijective [PerfectRing R p] : Function.Bijective (@WittVector.frobenius p R _ _) :=
  (frobeniusEquiv p R).bijective

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