$E^H/F$ is normal iff $H$ is a normal subgroup

Proved

GaloisFundamental.normal_fixedField_iff

by Lucas · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

field-theorygalois-theory

Let $E/F$ be a finite Galois extension with Galois group $G$ , and let $H \le G$ . Then the fixed field $E^H$ is a normal extension of $F$ if and only if $H$ is a normal subgroup of $G$ .

Preamble

import Mathlib

Formal statement

namespace GaloisFundamental

theorem normal_fixedField_iff (F E : Type*) [Field F] [Field E] [Algebra F E]
    [FiniteDimensional F E] [IsGalois F E] (H : Subgroup (E ≃ₐ[F] E)) :
    Normal F (IntermediateField.fixedField H) ↔ H.Normal := by sorry

end GaloisFundamental

Source

Wikipedia, "Fundamental theorem of Galois theory", revision oldid=1345286594, https://en.wikipedia.org/w/index.php?title=Fundamental_theorem_of_Galois_theory&oldid=1345286594, section "Properties of the correspondence", third bullet ("The field E^H is a normal extension of F ... if and only if H is a normal subgroup of Gal(E/F)")

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source and of the intended meaning. It is not the blind, independent auditor read-back the platform recommends, and no reviewer should treat it as independent evidence of faithfulness. Please compare the Lean code against the source yourself (or regenerate this read-back with an independent auditor) before confirming this item.

What is fixed. Arbitrary fields $F$ , $E$ with $E$ an $F$ -algebra, $E$ finite-dimensional over $F$ and Galois over $F$ ; $G$ = group of $F$ -algebra automorphisms of $E$ ; $H$ an arbitrary subgroup of $G$ . $E^H$ = fixed field of $H$ , viewed as a field extension of $F$ .

Assertion.

E^H / F \text{ is a normal extension} \quad\Longleftrightarrow\quad H \trianglelefteq G.

"Normal extension" is Mathlib's Normal: every element of $E^H$ is algebraic over $F$ and its minimal polynomial over $F$ splits in $E^H$ . " $H \trianglelefteq G$ " means $gHg^{-1} = H$ for all $g \in G$ . Only normality (not separability or Galois-ness) of $E^H/F$ appears in the statement.

Human review

Endorsed by Shuze Chen · Sep 28, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 28, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

EH/FE^H/FEH/F is normal iff HHH is a normal subgroup

$E^H/F$ is normal iff $H$ is a normal subgroup