bijective_frobenius

Mathlib.FieldTheory.Perfect

URI: https://scilib.ai/kg/mathlib#bijective_frobenius

English

If R is a perfect ring of characteristic p, then the Frobenius endomorphism x ↦ x^p is a bijection.

Русский

Для совершенного кольца R характеристик p эндоморфизм Фробениуса x ↦ x^p биективен.

LaTeX

$$Bijective( Frobenius_{R,p} )$$

Lean4

@[simp]
theorem bijective_frobenius : Bijective (frobenius R p) :=
  PerfectRing.bijective_frobenius

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru