Theorems · Definition · number theory

FiniteField.frobeniusAlgEquivOfAlgebraic

(K : Type u_1) →
  [inst : Field K] →
    [Fintype K] → (L : Type u_3) → [inst_2 : Field L] → [inst_3 : Algebra K L] → [Algebra.IsAlgebraic K L] → Gal(L/K)

If L/K is an algebraic extension of a finite field, the Frobenius K-algebra endomorphism of L is an automorphism.

Defined in

Mathlib.FieldTheory.Finite.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

FieldFintypeFieldAlgebraAlgebra.IsAlgebraic