TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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.

An algebraic extension generated by separable elements is separable

Statement

Let $K / F$ be algebraic and suppose $K = F (S)$ for a set $S$ of elements separable over $F$ . Then $K / F$ is separable.

Facts & Assumptions

Given: An algebraic extension $K = F (S)$ whose generators are separable over $F$ .

[L1]

An element is separable over $F$ when it is algebraic over $F$ and its minimal polynomial over $F$ is separable; the extension is separable when every element is (Separable algebraic elements and separable extensions).

[L2]

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

[L3]

The separable degree of a simple algebraic extension is the number of distinct roots of its generator's minimal polynomial (The separable degree of $F (α) / F$ is the number of distinct roots of $m_{α}$ ).

[L4]

The degree of a simple algebraic extension is the degree of that minimal polynomial (A simple algebraic extension is its minimal-polynomial quotient and has power basis $1, a, \dots, a^{n - 1}$ and degree $n$ ).

[L5]

Separable degree is multiplicative in finite towers (Separable degree is multiplicative in finite towers: $[L : F]_{s} = [L : K]_{s} [K : F]_{s}$ ).

[L6]

Ordinary degrees multiply in finite towers (Tower law for finite extensions: $[L : F] = [L : K] [K : F]$ ).

[L7]

Finitely many algebraic generators produce a finite extension (An extension generated by finitely many algebraic elements is finite).

[L8]

A finite extension is separable exactly when its separable degree equals its ordinary degree (A finite extension is separable if and only if $[K : F]_{s} = [K : F]$ ).

Proof

technique · direct

1.1L2

The union of $F (T)$ over the finite subsets $T \subseteq S$ is a subfield containing $F \cup S$ , so by [L2] it equals $F (S)$ . Hence every $a \in K$ lies in $E = F (s_{1}, \dots, s_{r})$ for finitely many $s_{i} \in S$ .

1.2L1L7

Put $E_{j} = F (s_{1}, \dots, s_{j})$ , so that $E_{0} = F$ , $E_{r} = E$ , and $E_{j} = E_{j - 1} (s_{j})$ . Each $s_{j}$ is algebraic over $F$ by [L1], so [L7] makes $E / F$ finite and every step of the tower finite.

2.1step 1.2L1L3L4

The minimal polynomial of $s_{j}$ over $E_{j - 1}$ divides its minimal polynomial over $F$ , which is separable by [L1]; a divisor of a polynomial with no repeated root has none, so the relative minimal polynomial has as many distinct roots as its degree. Hence [L3] and [L4] give $[E_{j} : E_{j - 1}]_{s} = [E_{j} : E_{j - 1}]$ at every step.

3.1step 1.2step 2.1L5L6L8

Multiplying these equalities over the tower, [L5] and [L6] give $[E : F]_{s} = [E : F]$ , so [L8] makes $E / F$ separable and the chosen $a$ separable over $F$ .

4.1step 1.1step 3.1L1L2∎

Since $a \in K$ was arbitrary, [L1] makes $K / F$ separable. If $S = \emptyset$ , [L2] gives $K = F$ , whose separable and ordinary degrees are both one, so the conclusion holds there as well.

Depends on

Used by

Dependency tree · two levels

28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

P. L. Clark, Field Theory, Chapters 4 and 5 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, Chapters 3 and 5 (standard reference, not scraped)