iterateFrobenius — Mathlib

English

The iterated Frobenius map x ↦ x^{p^n} is a ring endomorphism for a ring with CharP R p.

Русский

Итерированная карта Фробениуса x ↦ x^{p^n} является кольцевым эндоморфизмом кольца с CharP R p.

LaTeX

$$$\mathrm{iterateFrobenius}: R \to R, \ x \mapsto x^{p^n}$$$

Lean4

/-- The iterated Frobenius map `x ↦ x ^ p ^ n`. -/
def iterateFrobenius : R →+* R where
  __ := powMonoidHom (p ^ n)
  map_zero' := zero_pow (expChar_pow_pos R p n).ne'
  map_add' _ _ := add_pow_expChar_pow ..

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