frobeniusEquiv — Mathlib

English

There exists a ring equivalence frobeniusEquiv R p : R ≃+* R whose underlying map is x ↦ x^p.

Русский

Существует кольцевой эквивалент frobeniusEquiv R p : R ≃+* R, действующий как x ↦ x^p.

LaTeX

$$There exists a RingEquiv R R with Frobenius action$$

Lean4

/-- The Frobenius automorphism for a perfect ring. -/
@[simps! apply]
noncomputable def frobeniusEquiv : R ≃+* R :=
  RingEquiv.ofBijective (frobenius R p) PerfectRing.bijective_frobenius

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