bijective_iterateFrobenius

Mathlib.FieldTheory.Perfect

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

English

The iterated Frobenius map iterateFrobenius R p n is bijective.

Русский

Итеративный Фробениус iterateFrobenius R p n биективен.

LaTeX

$$Bijective( iterateFrobenius R p n )$$

Lean4

theorem bijective_iterateFrobenius : Bijective (iterateFrobenius R p n) :=
  coe_iterateFrobenius R p n ▸ (bijective_frobenius R p).iterate n

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

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

Разделы

Аффилиация

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