TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-02

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.

Multiplication of additive cosets is well defined if and only if the additive subgroup is a two-sided ideal

Statement

Multiplication of additive cosets is well defined if and only if the additive subgroup is a two-sided ideal.

Let $J \leq (R, +)$ . The rule $(r + J) (s + J) = r s + J$ is independent of representatives exactly when $J ⊴ R$ .

Facts & Assumptions

Given: A ring $R$ and an additive subgroup $J \leq (R, +)$ .

[L1]

The displayed rule is the proposed quotient multiplication (The quotient ring $R / I$ with $(r + I) (s + I) = r s + I$ ).

[L2]

A two-sided ideal is an additive subgroup absorbing multiplication on both sides (Left, right and two-sided ideals).

[L3]

Ring multiplication is distributive (In any ring $0 \cdot a = a \cdot 0 = 0$ , $(- a) b = a (- b) = - (a b)$ , $(- a) (- b) = a b$ , $(- 1) a = - a$ and $a (b - c) = a b - a c$ ).

[L4]

Coset equality is membership of a difference in the subgroup ( $x \in a H$ iff $a^{- 1} x \in H$ , and $a H = b H$ iff $a^{- 1} b \in H$ ).

[L5]

Additive cosets are available for an additive subgroup (The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ ).

Proof

technique · direct

1.1

If $J$ is an ideal and $r^{'} = r + i$ , $s^{'} = s + j$ , then $r^{'} s^{'} - r s = r j + i s + i j \in J$ , so the product is well defined.

L1L2L3L4L5givenalgebra

2.1

Conversely, compare $(r + J) (0 + J)$ with $(r + J) (j + J)$ and the reversed product; [L4] gives $r j, j r \in J$ for all $r, j$ .

step 1.1L1L2L3L4L5givenalgebra

3.1

Thus the rule is well defined exactly when $J$ is a two-sided ideal.

step 2.1∎

Depends on

Used by

For a two-sided ideal I, the additive cosets form a ring R/I with identity 1+I Theorem

Cited to discharge well-definedness by The quotient ring R/I with (r+I)(s+I)=rs+I.

Dependency tree · two levels

15 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

Ernst, An Inquiry-Based Approach to Abstract Algebra, Ideals and Quotient Rings (standard reference, not scraped)