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 be a finite extension. If all but possibly one of the generators are separable over , then is simple. In particular, every finite separable extension is simple.
Facts & Assumptions
Given: A finite extension in which all but possibly one generator are separable over .
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).
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).
Every finite extension of a finite field is simple (Every finite extension of a finite field is simple).
A field generated by finitely many algebraic elements is a finite extension (An extension generated by finitely many algebraic elements is finite).
An element is separable when its minimal polynomial has no repeated root (Separable algebraic elements and separable extensions).
Proof
For , one has , and for the displayed presentation is already simple. Assume . It is enough to combine two generators: if 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].
If is finite, the two-generator extension is simple by [L3].
Suppose is infinite. In a common splitting field from [L2], list the distinct conjugates of and the pairwise distinct conjugates of the separable element . Choose a nonzero avoiding the finitely many values with , and put .
In , the minimal polynomial of and the translated minimal polynomial of have as a common root. By the choice of , any common root would give and hence must be ; [L1] therefore makes their monic gcd . Thus and then .
Hence 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.
Depends on
- Separable algebraic elements and separable extensions
- The monic gcd of two base-field polynomials is unchanged after extending the coefficient field
- Every finite family of nonzero polynomials has a splitting field, obtained from their product
- Every finite extension of a finite field is simple
- An extension generated by finitely many algebraic elements is finite
Used by
- A finite separable extension has only finitely many intermediate fields Corollary
- Every finite extension of a perfect field is simple Corollary
- The one-step root condition makes an algebraic extension of a perfect field algebraically closed Lemma
- 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: 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
- J. S. Milne, Fields and Galois Theory, Theorem 5.1 (standard reference, not scraped)
- P. L. Clark, Field Theory, Chapter 5 (standard reference, not scraped)