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 extension generated by finitely many algebraic elements is finite
Statement
If are algebraic over , then is finite.
Facts & Assumptions
Given: A field extension containing elements algebraic over .
The field is obtained by adjoining the finite list of generators (Finitely generated field extensions ).
An algebraic element generates a finite simple extension (An element is algebraic over if and only if its simple extension is finite).
Degrees multiply in a finite tower (Tower law for finite extensions: ).
An element algebraic over satisfies a nonzero polynomial in (Algebraic and transcendental elements and algebraic extensions).
Proof
Put and for . By [L4], the nonzero polynomial over satisfied by also belongs to , so is algebraic over . Thus [L2] makes finite.
Repeated application of [L3] makes finite, with degree equal to the product of the simple-step degrees.
By [L1], . If , this is of degree one, so the boundary case also holds.
Depends on
Used by
- A field finitely generated as a k-algebra is a finite extension of k Corollary
- The algebraic numbers in ℂ form an algebraic closure of ℚ Corollary
- Separating transcendence basis and separably generated extensions Definition
- A finite-type field has finite relative algebraic constants Lemma
- Conjugates of an average of roots of unity Lemma
- Finite purely inseparable rational extensions admit a finite Frobenius envelope Lemma
- Integral closure in a purely inseparable rational envelope is finite Lemma
- Separable generation after finite purely inseparable extensions Lemma
- The one-step root condition makes an algebraic extension of a perfect field algebraically closed Lemma
- Unramified residue extensions are finite separable Lemma
- For finite subextensions in a common field, [EE':F]≤ [E:F][E':F] Proposition
- A finite extension generated by elements all but possibly one of which are separable is simple Theorem
- A finite-type domain over a field has finite normalization Theorem
- Algebraicity is transitive in towers of field extensions Theorem
- An algebraic extension generated by separable elements is separable Theorem
- Assuming Choice, every field has an algebraic extension containing roots of all nonconstant base polynomials Theorem
- Assuming Choice, separable closures exist and are base-isomorphic Theorem
- Differentials of a separably generated field extension Theorem
- Finitely generated extensions of a perfect field are separably generated Theorem
- Polynomial algebras over fields have finite integral closures Theorem
- Separability is transitive in towers of algebraic extensions Theorem
- The complex numbers are algebraically closed Theorem
- The elements of an extension algebraic over the base field form a subfield Theorem
- The normal closure of a finite extension exists and is finite Theorem
Dependency tree · two levels
11 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)