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 field is algebraically closed exactly when every nonconstant polynomial splits, equivalently when it has no nontrivial finite extension
Statement
For a field , the following are equivalent:
- is algebraically closed.
- Every nonconstant polynomial in splits over .
- has no nontrivial finite extension.
Facts & Assumptions
Given: A field .
A field is algebraically closed exactly when every nonconstant polynomial over it has a root in the field (An algebraically closed field: every nonconstant polynomial has a root in the field).
Splitting means factorization into linear factors over the field (Polynomials that split and splitting fields of a polynomial or a family of polynomials).
A polynomial has as a root exactly when divides (Factor theorem over a commutative ring).
An element is algebraic over if and only if its simple extension over is finite (An element is algebraic over if and only if its simple extension is finite).
Every nonconstant polynomial over has a root in some extension of (Every nonconstant polynomial over a field has a root in some field extension).
Every element of a finite extension is algebraic over the base field (Every finite field extension is algebraic).
Every algebraic element has a unique monic irreducible minimal polynomial, and a polynomial vanishes at that element exactly when the minimal polynomial divides it (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).
Proof
Assume is algebraically closed, and let be nonconstant. By [L1] it has a root , so [L3] gives for some . Repeating the same argument on while it remains nonconstant writes as a product of linear factors, so splits over in the sense of [L2].
Assume every nonconstant polynomial in splits over , and let be finite. For any , fact [L6] makes algebraic over . If , let be its minimal polynomial over . Then [L7] makes a nonconstant irreducible polynomial with . By the hypothesis, splits over and therefore has a root . Fact [L3] gives as a linear factor of , contradicting irreducibility. Hence every already lies in , so .
Assume has no nontrivial finite extension, and let be nonconstant. By [L5] there is an extension and an element with . Then is algebraic over , so [L4] makes finite. By the hypothesis this finite extension must be trivial, hence . Therefore every nonconstant polynomial over has a root in , and [L1] says that is algebraically closed.
Steps 1.1, 1.2, and 1.3 prove , so the three conditions are equivalent.
Depends on
An algebraically closed field: every nonconstant polynomial has a root in the field
Polynomials that split and splitting fields of a polynomial or a family of polynomials
Factor theorem over a commutative ring
An element is algebraic over if and only if its simple extension is finite
Every nonconstant polynomial over a field has a root in some field extension
Every finite field extension is algebraic
The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element