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.
For every field , is a principal ideal domain
Statement
For every field , every ideal of is generated by one polynomial; equivalently, is a principal ideal domain.
Facts & Assumptions
Given: A field .
The ring is a Euclidean domain with degree as Euclidean function (For every field , is a Euclidean domain with degree as Euclidean function).
Every Euclidean domain is a principal ideal domain (Every Euclidean domain is a principal ideal domain).
A principal ideal domain is an integral domain in which every ideal is principal (Principal ideal domain).
Proof
By [L1] and [L2], is a principal ideal domain.
Unfolding [L3], every ideal of therefore has the form for some polynomial .
Depends on
Used by
- Invariant factors and elementary divisors of an endomorphism Definition
- The monic greatest common divisor of two polynomials over a field Definition
- The truncated polynomial ring k[x]/(xⁿ) is local Artinian of length n Example
- A prime chain in R[x] has length at most one more than its contraction chain Lemma
- Only one saturated step can lie over a fixed contracted prime in R[x] Lemma
- The vector annihilator is the unique monic generator of Ann_T(v) and divides the minimal polynomial Proposition
- The annihilator ideal is nonzero and has a unique monic generator; p(T)=0 if and only if μ_T∣ p Theorem
- The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element 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
- Thomas W. Judson, Abstract Algebra: Theory and Applications, Theorem 17.20 (standard reference, not scraped)