instIsCyclicAlgEquivOfFinite — Mathlib

English

For finite L over K, the group of K-algebra automorphisms of L is cyclic, generated by the Frobenius automorphism frobeniusAlgEquivOfAlgebraic K L.

Русский

Для конечного расширения L/K группа автоморфизмов над K циклическая и порождается автоморфизмом Фробениуса frobeniusAlgEquivOfAlgebraic K L.

LaTeX

$$$\\operatorname{IsCyclic}\\left(\\operatorname{AlgEquiv}_K(L,L)\\right)$$$

Lean4

instance (K L) [Finite L] [Field K] [Field L] [Algebra K L] : IsCyclic (L ≃ₐ[K] L) where
  exists_zpow_surjective :=
    have := Finite.of_injective _ (algebraMap K L).injective
    have := Fintype.ofFinite K
    ⟨frobeniusAlgEquivOfAlgebraic K L, fun f ↦
      have ⟨n, hn⟩ := (bijective_frobeniusAlgEquivOfAlgebraic_pow K L).2 f;
      ⟨n, hn⟩⟩

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