iterate_frobenius

Mathlib.Algebra.CharP.Frobenius

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

English

The nth iterate of Frobenius equals repeated power: (frobenius R p)^[n] x = x^{p^n}.

Русский

n-ая итерация Фробениуса равна повторной степени: (frobenius R p)^[n] x = x^{p^n}.

LaTeX

$$$\\\\left( frobenius R p \\right)^{[n]}(x) = x^{p^n}$$$

Lean4

theorem iterate_frobenius : (frobenius R p)^[n] x = x ^ p ^ n :=
  congr_fun (pow_iterate p n) x

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

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

Разделы

Аффилиация

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