Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

The one-step root condition makes an algebraic extension of a perfect field algebraically closed

Statement

Let F be perfect and let L/F be algebraic. If every nonconstant polynomial in F[x] has a root in L, then L is algebraically closed.

Facts & Assumptions

Given: A perfect field F and an algebraic extension L/F in which every nonconstant polynomial over F has a root.

[L1]

Algebraic extensions of perfect fields are separable (Every algebraic extension of a perfect field is separable).

[L3]

A root of an irreducible polynomial induces the unique base-field embedding of the corresponding simple extension (Universal property of adjoining a root of an irreducible polynomial).

[L4]

Every nonzero polynomial has a splitting field (Every nonzero polynomial over a field has a splitting field).

[L5]

Algebraicity is transitive in towers (Algebraicity is transitive in towers of field extensions).

[L6]

A field is algebraically closed when every nonconstant polynomial over it has a root in it (An algebraically closed field: every nonconstant polynomial has a root in the field).

[L7]

A field generated by finitely many algebraic elements is finite over its base (An extension generated by finitely many algebraic elements is finite).

Proof

technique · direct
1.1L1L2L4L7

Let f∈F[x] be irreducible and nonconstant, and choose a splitting field E/F by [L4]. It is generated by the finitely many roots of f, so [L7] makes it finite; [L1] makes it separable and [L2] gives E=F(α) for some α.

2.1step 1.1L3

The minimal polynomial mα∈F[x] has a root β∈L by hypothesis. By [L3] there is an F-embedding E=F(α)→L sending α to β. Since f splits in E and its coefficients are fixed, it splits in the image inside L.

3.1step 2.1algebra

Thus every irreducible polynomial over F, and hence every polynomial over F, splits in L.

4.1step 3.1L4L5

Let q∈L[x] be nonconstant and choose a root γ in a splitting field by [L4]. The element γ is algebraic over L, while L/F is algebraic, so [L5] makes γ algebraic over F. Its minimal polynomial over F splits in L by step 3.1; since γ is one of its roots, γ∈L.

5.1step 4.1L6∎

Every nonconstant polynomial over L therefore has a root in L, so [L6] makes L algebraically closed.

Depends on

Used by

Dependency tree · two levels

27 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