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.
The Noetherian minimal-prime induction split
Statement
Let be a commutative ring and let be a proper radical ideal that is not prime. Then there exist elements with . For any such choice of and , every prime ideal minimal over is minimal over or minimal over .
Facts & Assumptions
Given: A commutative ring and a proper radical ideal that is not prime.
A prime ideal is proper and contains one factor whenever it contains a product (Prime ideals and maximal ideals in a commutative ring).
Proof
Because is not prime, [L1] gives elements with but and .
Let be a prime ideal minimal over . Since and is prime, [L1] gives or . If and is a prime ideal with , then , so minimality of over forces . Thus is minimal over . The same argument with in place of shows that if , then is minimal over .
Therefore every prime ideal minimal over appears on one side of the split or .
Depends on
Used by
Dependency tree · two levels
5 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
- M. Hochster, Introduction to Commutative Algebra, Math 614 notes (2020) (standard reference, not scraped)
- The Stacks Project, Section 10.31: Noetherian rings (standard reference, not scraped)