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.
For a two-sided ideal , the additive cosets form a ring with identity
Statement
For a two-sided ideal , the additive cosets form a ring with identity .
Facts & Assumptions
Given: A ring and a two-sided ideal .
has the stated coset addition and multiplication (The quotient ring with ).
This multiplication is well defined for a two-sided ideal (Multiplication of additive cosets is well defined if and only if the additive subgroup is a two-sided ideal).
The additive cosets already form a group (For , the cosets form a group with identity and inverse ).
Associativity and distributivity hold in (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides).
Proof
By [L3], coset addition has an abelian-group structure, and [L2] makes coset multiplication a defined operation.
Associativity and both distributive laws follow by applying the corresponding ring law in to representatives; is a multiplicative identity.
Hence is a ring with identity .
Depends on
- The quotient ring $R/I$ with $(r+I)(s+I)=rs+I$
- Multiplication of additive cosets is well defined if and only if the additive subgroup is a two-sided ideal
- For $N\mathrel{\trianglelefteq}G$, the cosets form a group with identity $N$ and inverse $(gN)^{-1}=g^{-1}N$
- Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides
Used by
- If I⊆ J are ideals of R, then J/I is an ideal of R/I Lemma
- The canonical projection R→ R/I is a surjective ring homomorphism with kernel I Proposition
- Correspondence theorem: ideals of R/I correspond to ideals of R containing I Theorem
- R/M is a field if and only if M is a maximal ideal Theorem
- R/P is an integral domain if and only if P is a prime ideal Theorem
Cited to discharge well-definedness by The quotient ring R/I with (r+I)(s+I)=rs+I.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 26 results over 16 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
- Ernst, An Inquiry-Based Approach to Abstract Algebra, Ideals and Quotient Rings (standard reference, not scraped)