Degrees in the Galois correspondence: $[E:E^H] = |H|$ and $[E^H:F] = [G:H]$

Proved

GaloisFundamental.finrank_fixedField

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$ be a subgroup. Then

[E : E^H] = |H| \qquad\text{and}\qquad [E^H : F] = [G : H].

Preamble

import Mathlib

Formal statement

namespace GaloisFundamental

theorem finrank_fixedField (F E : Type*) [Field F] [Field E] [Algebra F E]
    [FiniteDimensional F E] [IsGalois F E] (H : Subgroup (E ≃ₐ[F] E)) :
    Module.finrank (IntermediateField.fixedField H) E = Nat.card H ∧
      Module.finrank F (IntermediateField.fixedField H) = H.index := 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", second bullet ("if H is a subgroup of Gal(E/F), then |H| = [E:E^H] and |Gal(E/F)/H| = [E^H: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$ , $E/F$ Galois (separable and normal); $G$ = group of $F$ -algebra automorphisms of $E$ ; $H$ an arbitrary subgroup of $G$ . $E^H$ = fixed field of $H$ .

Assertion. Both equalities of natural numbers hold:

\dim_{E^H} E = |H| \qquad\text{and}\qquad \dim_F E^H = [G : H].

Here $\dim_{E^H} E$ is the dimension of $E$ as a vector space over the subfield $E^H$ (Mathlib's finrank, which would be $0$ for an infinite-dimensional space, but all spaces here are finite-dimensional), $|H|$ is the cardinality of $H$ (Mathlib's Nat.card, finite here), and $[G:H]$ is the index of $H$ in $G$ (Mathlib's Subgroup.index, the number of cosets, finite here). Edge cases $H = \{1\}$ (giving $[E:E]=1$ and $[E:F] = |G|$ ) and $H = G$ are included.

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

Degrees in the Galois correspondence: [E:EH]=∣H∣[E:E^H] = |H|[E:EH]=∣H∣ and [EH:F]=[G:H][E^H:F] = [G:H][EH:F]=[G:H]

Degrees in the Galois correspondence: $[E:E^H] = |H|$ and $[E^H:F] = [G:H]$