frobeniusAlgEquivOfAlgebraic — Mathlib

English

The order of the Frobenius K-algebra equivalence for an algebraic finite extension L/K equals the K-dimension (finrank) of L over K.

Русский

Порядок эквивалентности Фробениуса K на алгебраическом конечном расширении L/K равен размерности L над K (finrank).

LaTeX

$$orderOf (frobeniusAlgEquivOfAlgebraic K L) = Module.finrank K L$$

Lean4

/-- If `L/K` is an algebraic extension of a finite field, the Frobenius `K`-algebra endomorphism
  of `L` is an automorphism. -/
@[simps!]
noncomputable def frobeniusAlgEquivOfAlgebraic [Algebra.IsAlgebraic K L] : L ≃ₐ[K] L :=
  (Algebra.IsAlgebraic.algEquivEquivAlgHom K L).symm (frobeniusAlgHom K L)

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