iterateFrobenius_def

Mathlib.Algebra.CharP.Frobenius

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

English

Iterating Frobenius n times yields x^{p^n}.

Русский

Повторное применение Фробениуса n раз даёт x^{p^n}.

LaTeX

$$$\\\\text{iterateFrobenius } R\\ p\\ n (x) = x^{p^n}$$$

Lean4

theorem iterateFrobenius_def : iterateFrobenius R p n x = x ^ p ^ n :=
  rfl

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

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

Разделы

Аффилиация

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