CorollaryStatement: 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.

For a finite extension, $[K : F]_{s} \leq [K : F]$

Statement

For every finite field extension $K / F$ , one has $[K : F]_{s} \leq [K : F]$ .

Facts & Assumptions

Given: A finite extension $K / F$ .

[L1]

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

[L2]

Embeddings of a simple algebraic extension correspond to the distinct roots of its minimal polynomial ( $F$ -embeddings of $F (α)$ into an algebraically closed field correspond to the distinct roots of $m_{α}$ ).

[L3]

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

[L4]

A finite extension has a finite basis 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$ by [L4]; its elements generate $K$ , so adjoining them successively gives a finite tower of simple extensions from $F$ to $K$ .

L4choose

1.2

At each simple step, [L2] counts embeddings by distinct roots of a minimal polynomial, so its separable degree is at most the degree of that polynomial, which is the ordinary degree of the step.

2.1

Multiplying the inequalities in step 1.2 and using [L1] and [L3] for the two tower products gives $[K : F]_{s} \leq [K : F]$ .

step 1.1step 1.2L1L3algebra∎

Depends on

Used by

A finite extension is separable if and only if [K:F]ₛ=[K:F] Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 41 results over 12 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

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)

For a finite extension, [K:F]s≤[K:F][K:F]s​≤[K:F]