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.
Finitely generated field extensions
Definition
Let be a field extension and let . The notation
means the smallest subfield of containing and all the . An extension is finitely generated when for some finite list. For the empty list, .
Depends on
Used by
- Geometrically regular algebras and geometrically regular fibres Definition
- Separating transcendence basis and separably generated extensions Definition
- The cyclotomic extension K(μₙ) as a splitting field of tⁿ-1 Definition
- A dominant map has a surjective differential on a dense source open Lemma
- A finite normal extension is separable over its purely inseparable fixed field Lemma
- A finite-type field has finite relative algebraic constants Lemma
- A finite-type field reduces to a localization over a transcendence basis Lemma
- Finite purely inseparable rational extensions admit a finite Frobenius envelope Lemma
- Finite-type field extensions with zero Ω Lemma
- Function field of an integral finite-type scheme Lemma
- Integral closure in a purely inseparable rational envelope is finite Lemma
- Separable generation after finite purely inseparable extensions Lemma
- Unramified residue extensions are finite separable Lemma
- A finite-type domain over a field has finite normalization Theorem
- An extension generated by finitely many algebraic elements is finite Theorem
- Finitely generated extensions of a perfect field are separably generated Theorem
- For gcd(n,q)=1 the reduction of Φₙ in F_q[t] is a product of distinct monic irreducibles, each of degree the order of [q] modulo n Theorem
- K(μₘ)K(μₙ)=K(μ_lcm(m,n)) Theorem
- Polynomial algebras over fields have finite integral closures Theorem
- tⁿ-1 is separable over K exactly when the characteristic does not divide n, and then a splitting field carries n distinct n-th roots of unity Theorem
Dependency tree · two levels
13 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)