of_fixedField_eq_bot — Mathlib

English

Let E/F be a finite extension of fields. If the fixed field of E under all F-automorphisms of E is F, then E/F is Galois.

Русский

Пусть E/F — конечное расширение полей. Если фиксированное поле E по всем F-автоморфизмам E равно F, то расширение E/F галуа.

LaTeX

$$$\operatorname{finrank}_F E < \infty \;\wedge\; \operatorname{FixedField}(\operatorname{Aut}_F(E)) = F \;\Rightarrow\; E/F \text{ is Galois}$$$

Lean4

theorem of_fixedField_eq_bot [FiniteDimensional F E] (h : IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥) :
    IsGalois F E := by
  rw [← isGalois_iff_isGalois_bot, ← h]
  classical exact IsGalois.of_fixed_field E (⊤ : Subgroup (E ≃ₐ[F] E))

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