iterateFrobenius_def

Mathlib.Algebra.CharP.Frobenius

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

English

For algebras R,S and n, the iterated Frobenius map satisfies the rule x ↦ x^{p^n}.

Русский

Для алгебр R,S и натурального n хорошо определяется: x ↦ x^{p^n}.

LaTeX

$$$\operatorname{iterateFrobenius}_{R,S}(p,n)(x) = x^{p^n}$$$

Lean4

theorem iterateFrobenius_def [Algebra R S] (n : ℕ) (x : S) : iterateFrobenius R S p n x = x ^ p ^ n :=
  rfl

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

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

Разделы

Аффилиация

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