Theorems · Definition · number theory

FiniteField.frobeniusAlgEquiv

(K : Type u_1) →
  (R : Type u_2) →
    [inst : Field K] →
      [Fintype K] →
        [inst_2 : CommRing R] → [inst_3 : Algebra K R] → (p : ℕ) → [ExpChar R p] → [PerfectRing R p] → R ≃ₐ[K] R

If R is a perfect ring and an algebra over a finite field K, the Frobenius K-algebra endomorphism of R is an automorphism.

Defined in

Mathlib.FieldTheory.Finite.Basic

Cited by

2 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFintypeCommRingAlgebraExpCharPerfectRing