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 with
Multiplication of additive cosets is well defined if and only if the additive subgroup is a two-sided ideal
For , the cosets form a group with identity and inverse
Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides