TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The normal closure of a finite extension exists and is finite

Statement

Let $K / F$ be a finite extension embedded in an algebraic closure $Ω$ of $F$ . Its normal closure in $Ω$ is a finite extension of $F$ . If $K = F (α_{1}, \dots, α_{r})$ , it is the splitting field in $Ω$ of the product of the minimal polynomials of the $α_{i}$ .

Facts & Assumptions

Given: A finite extension $F \subseteq K \subseteq Ω$ with $Ω / F$ an algebraic closure.

[L1]

The normal closure is the intersection of the normal intermediate extensions containing $K$ (The normal closure of an algebraic extension inside a fixed algebraic closure).

[L2]

A finite family of nonzero polynomials has a splitting field (Every finite family of nonzero polynomials has a splitting field, obtained from their product).

[L3]

An algebraic splitting extension is normal (An algebraic extension that is a splitting field of a polynomial is normal).

[L4]

A field generated by finitely many algebraic elements is finite over the base (An extension generated by finitely many algebraic elements is finite).

[L5]

A finite extension is finite-dimensional over its base (The degree $[K : F] = \dim_{F} K$ of a finite field extension).

Proof

technique · direct

1.1

Choose a finite $F$ -basis of $K$ using [L5]; it is also a finite generating family $α_{1}, \dots, α_{r}$ . Let $f_{i}$ be the minimal polynomial of $α_{i}$ over $F$ , and inside $Ω$ let $E$ be the field generated by all roots of $f_{1} \dots f_{r}$ .

L2L5choose

2.1

The field $E$ is generated by finitely many algebraic roots, so [L4] makes $E / F$ finite. It is a splitting field of the product and is normal by [L3], and it contains every $α_{i}$ , hence $K$ .

step 1.1L3L4

2.2

If $H / F$ is any normal intermediate extension in $Ω$ containing $K$ , then each $f_{i}$ , having the root $α_{i} \in H$ , splits in $H$ . Thus $H$ contains all generators of $E$ and $E \subseteq H$ .

step 1.1algebra

3.1

Therefore $E$ is contained in every field intersected in [L1], while step 2.1 makes $E$ one of those fields. It equals the normal closure, which is consequently finite.

step 2.1step 2.2L1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 55 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

The Stacks Project, Section 9.15: Normal extensions (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, Chapter 6 (standard reference, not scraped)