Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

A finite extension generated by elements all but possibly one of which are separable is simple

Statement

Let E=F(α1,,αr) be a finite extension. If all but possibly one of the generators are separable over F, then E/F is simple. In particular, every finite separable extension is simple.

Facts & Assumptions

Given: A finite extension E=F(α1,,αr) in which all but possibly one generator are separable over F.

[L1]

A polynomial gcd computed over a field is unchanged after extending the coefficient field (The monic gcd of two base-field polynomials is unchanged after extending the coefficient field).

[L2]

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

[L3]

Every finite extension of a finite field is simple (Every finite extension of a finite field is simple).

[L4]

A field generated by finitely many algebraic elements is a finite extension (An extension generated by finitely many algebraic elements is finite).

[L5]

An element is separable when its minimal polynomial has no repeated root (Separable algebraic elements and separable extensions).

Proof

technique · direct
1.1

For r=0, one has E=F=F(0), and for r=1 the displayed presentation is already simple. Assume r2. It is enough to combine two generators: if F(α,β)=F(γ) whenever β is separable, repeated combination leaves at most the originally exceptional generator as the first entry and a separable generator as the second. Finiteness of each intermediate extension follows from [L4].

givenL4L5
1.2

If F is finite, the two-generator extension is simple by [L3].

L3
1.3

Suppose F is infinite. In a common splitting field from [L2], list the distinct conjugates αi of α and the pairwise distinct conjugates βj of the separable element β. Choose a nonzero cF avoiding the finitely many values (α1αi)/(βjβ1) with βjβ1, and put γ=α+cβ.

L2L5choose
2.1

In F(γ)[x], the minimal polynomial of α and the translated minimal polynomial of β have α as a common root. By the choice of c, any common root would give αi+cβj=α+cβ and hence must be α; [L1] therefore makes their monic gcd xα. Thus αF(γ) and then β=(γα)/cF(γ).

step 1.3L1algebra
3.1

Hence F(α,β)=F(γ) over either a finite or an infinite base. Iterating step 1.1 proves the theorem, and when every generator is separable it gives the usual finite separable primitive-element theorem.

step 1.1step 1.2step 2.1

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 68 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