English
The iterated Frobenius map is a semilinear map that, on an algebra, acts as the p-th power after n iterations.
Русский
Итерированный Фробениус отображает элемент алгебры в его p-ю степень после n итерирования.
LaTeX
$$$\text{iterateFrobenius}_{R,S}(p,n): S \to S$ is the semilinear iterated Frobenius map with underlying action $x \mapsto x^{p^n}$$$
Lean4
/-- The iterated Frobenius map of an algebra as an iterated-Frobenius-semilinear map. -/
nonrec def iterateFrobenius [Algebra R S] : S →ₛₗ[iterateFrobenius R p n] S
where
__ := iterateFrobenius S p n
map_smul' f
s := show iterateFrobenius S p n _ = _ by simp_rw [iterateFrobenius_def, Algebra.smul_def, mul_pow, ← map_pow]; rfl