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 simple transcendental extension consists exactly of rational expressions in its generator
Statement
If is a field extension and is transcendental over , then
Facts & Assumptions
Given: A field extension and an element transcendental over .
For transcendental , evaluation has zero kernel (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).
is the smallest subfield of containing and (Field extensions, generated subrings , generated subfields , and simple extensions).
Transcendental means that no nonzero polynomial in vanishes at (Algebraic and transcendental elements and algebraic extensions).
Proof
Let be the set on the right. By [F1], implies , so every displayed quotient is defined.
The choices and show that .
Common denominators show that is closed under addition, subtraction, and multiplication.
If , then by [A1], and its inverse is .
Conversely, every subfield containing and contains , , and for every with ; hence it contains .
Thus is a subfield of containing and , so by [F2].
In particular , and step 3.1 gives equality.
Depends on
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 29 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- J. S. Milne, Fields and Galois Theory (standard reference, not scraped)