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 Noetherian ring has finitely many minimal prime ideals
Statement
Let be a Noetherian commutative ring. Then has only finitely many minimal prime ideals.
This theorem inherits only the dependent-choice cost already recorded in the cited Noetherian-induction corollary.
Facts & Assumptions
Given: A Noetherian commutative ring .
The nilradical is , and every ideal of the form is radical (The nilradical and reduced rings, The radical of an ideal is an ideal).
Every radical ideal of a Noetherian ring is a finite intersection of its minimal primes, and hence has only finitely many minimal primes (A radical ideal in a Noetherian ring is a finite intersection of minimal primes).
Proof
Let . By [L1], is a radical ideal, so [L2] gives only finitely many prime ideals minimal over .
A prime ideal contains if and only if it contains every nilpotent element, hence if and only if it contains . Therefore the prime ideals minimal over are exactly the prime ideals minimal over .
Combining steps 1.1 and 1.2 shows that has only finitely many minimal prime ideals.