iterateFrobeniusEquiv — Mathlib

English

The iterated Frobenius automorphism is defined by composing the base Frobenius automorphism n times.

Русский

Итеративный Фробениус-автоморфизм задаётся как композиция базового Фробениуса n раз.

LaTeX

$$iterateFrobeniusEquiv R p n : R ≃+* R$$

Lean4

/-- The iterated Frobenius automorphism for a perfect ring. -/
@[simps! apply]
noncomputable def iterateFrobeniusEquiv : R ≃+* R :=
  RingEquiv.ofBijective (iterateFrobenius R p n) (bijective_iterateFrobenius R p n)

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