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

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.

An algebraic extension generated by elements whose minimal polynomials split in it is normal

Statement

Let $E / F$ be algebraic and suppose $E = F (T)$ for a subset $T \subseteq E$ . If the minimal polynomial over $F$ of every $t \in T$ splits over $E$ , then $E / F$ is normal.

Facts & Assumptions

Given: An algebraic extension $E / F$ , a generating set $T$ , and the splitting hypothesis in the Statement.

[F1]

The field $F (T)$ is the smallest subfield containing $F \cup T$ (Field extensions, generated subrings $F [S]$ , generated subfields $F (S)$ , and simple extensions).

[F2]

Every element algebraic over $F$ has a unique monic irreducible minimal polynomial (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

[F3]

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

[F4]

Normality means that the minimal polynomial of every element of the extension splits there (A normal algebraic extension is one in which every minimal polynomial with a root in the extension splits there).

Proof

technique · finite-support reduction

1.1

The union $U = ⋃_{T_{0} \subseteq T, T_{0} finite} F (T_{0})$ is a subfield of $E$ : sums, products, inverses, and pairs of elements lie in the field generated by the union of their two finite supports. It contains $F \cup T$ , so [F1] gives $E = F (T) \subseteq U$ , while the reverse inclusion is immediate.

2.1

Fix $β \in E$ . By step 1.1, choose a finite set $T_{0} = {t_{1}, \dots, t_{m}} \subseteq T$ with $β \in F (T_{0})$ . Let $p_{j}$ be the minimal polynomial of $t_{j}$ over $F$ , and let $K \subseteq E$ be the field generated by all roots in $E$ of the product $p_{1} \dots p_{m}$ . If $m = 0$ , take the product to be $1$ and $K = F$ .

F2step 1.1

3.1

Each $p_{j}$ splits over $E$ by hypothesis. Their product is monic and hence nonzero, so $K$ is its splitting field and contains every $t_{j}$ ; hence $β \in F (T_{0}) \subseteq K$ . Also $K / F$ is algebraic because $K \subseteq E$ and $E / F$ is algebraic. By [F3], $K / F$ is normal.

F3step 2.1algebra

4.1

Let $m_{β}$ be the minimal polynomial of $β$ over $F$ . Since $β \in K$ and $K / F$ is normal, $m_{β}$ splits over $K$ , hence over $E$ . This holds for every $β \in E$ , so [F4] proves that $E / F$ is normal.

F4step 3.1∎

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: 44 results over 14 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, Lemma 9.15.11 (standard reference, not scraped)