iterateFrobeniusEquiv_def

Mathlib.FieldTheory.Perfect

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

English

The action of iterateFrobeniusEquiv on x is x^{p^n}.

Русский

Действие iterateFrobeniusEquiv на x равно x^{p^n}.

LaTeX

$$iterateFrobeniusEquiv_def (x) : iterateFrobeniusEquiv R p n x = x^{p^{n}}$$

Lean4

theorem iterateFrobeniusEquiv_def (x : R) : iterateFrobeniusEquiv R p n x = x ^ p ^ n :=
  rfl

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

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

Разделы

Аффилиация

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