Alphabeta MathHow 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.
An element is algebraic over if and only if its simple extension is finite
Statement
For an element of an extension ,
If is algebraic with minimal polynomial of degree , then .
Facts & Assumptions
Given: A field extension and an element .
If is algebraic with minimal polynomial of degree , then is a basis of and its degree is (A simple algebraic extension is its minimal-polynomial quotient and has power basis and degree ).
Every element of a finite extension is algebraic over the base (Every finite field extension is algebraic).
Proof
If is algebraic, [L1] gives a finite power basis of and the stated degree.
Conversely, if is finite, [L2] says every element of , in particular , is algebraic over .
These are the two implications of the equivalence.
Depends on
Used by
- The algebraic numbers in ℂ form an algebraic closure of ℚ Corollary
- Fₚ is the union of its finite subfields and is an infinite algebraic extension Example
- FALSE: every algebraic extension is simple False statement
- A finite-type field has finite relative algebraic constants Lemma
- A field is algebraically closed exactly when every nonconstant polynomial splits, equivalently when it has no nontrivial finite extension Proposition
- The relative algebraic closure of F in K has no further algebraic elements inside K Proposition
- A monic irreducible of degree d over F_q has the d distinct roots α,α^q,…,α^qᵈ⁻¹ Theorem
- A real number is algebraically constructible exactly when it lies in a finite tower of real quadratic adjunctions Theorem
- Algebraicity is transitive in towers of field extensions Theorem
- An extension generated by finitely many algebraic elements is finite Theorem
- Finite and finite type etale schemes over an algebraically closed field Theorem
- The complex numbers are algebraically closed Theorem
Dependency tree · two levels
10 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
- A. W. Knapp, Basic Algebra, 2nd ed., Chapter IX, Section 1 (standard reference, not scraped)