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.
In a nonzero commutative ring, every proper ideal is contained in a maximal ideal
Statement
Assume the Axiom of Choice (The Axiom of Choice).
In a nonzero commutative ring, every proper ideal is contained in a maximal ideal.
Facts & Assumptions
Given: A nonzero commutative ring and a proper ideal .
A maximal ideal is a maximal proper ideal under inclusion (Prime ideals and maximal ideals in a commutative ring).
Ideals are additive subgroups with multiplication absorption (Left, right and two-sided ideals).
An ideal criterion and intersection closure are available (Ideal criteria and intersections of ideals).
Assuming the Axiom of Choice, a nonempty poset in which every chain has an upper bound has a maximal element (Zorn's lemma).
A chain is a subset linearly ordered by the ambient order (Chain in a poset).
A maximal element has no strictly larger element in the poset (Maximal element and greatest element).
A nonzero ring has and ring operations distribute (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides).
Proof
Let be the poset of proper ideals of containing , ordered by inclusion.
is nonempty, because is a proper ideal containing .
The empty chain of has an upper bound in : every member of is vacuously above all of its members, and is nonempty, so is such an upper bound.
A nonempty chain has an upper bound in : is an ideal containing , and it is proper, since would place in some member of , forcing that member to equal and contradicting its properness.
Every chain of has an upper bound in , and is a nonempty poset, so Zorn's lemma yields a maximal element of .
is a proper ideal containing that is maximal among proper ideals of , so is a maximal ideal containing .
Depends on
Prime ideals and maximal ideals in a commutative ring
Left, right and two-sided ideals
Ideal criteria and intersections of ideals
Zorn's lemma
The Axiom of Choice
Chain in a poset
Maximal element and greatest element
Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides