iterateFrobenius — Mathlib

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

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