Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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≤(R,+)J\le(R,+). The rule (r+J)(s+J)=rs+J(r+J)(s+J)=rs+J is independent of representatives exactly when J⊴RJ\mathrel{\trianglelefteq}R.

Facts & Assumptions

Given: A ring RR and an additive subgroup J≤(R,+)J\le(R,+).

[L1]

The displayed rule is the proposed quotient multiplication (The quotient ring R/IR/I with (r+I)(s+I)=rs+I(r+I)(s+I)=rs+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⋅a=a⋅0=00 \cdot a = a \cdot 0 = 0, (−a)b=a(−b)=−(ab)(-a)b = a(-b) = -(ab), (−a)(−b)=ab(-a)(-b) = ab, (−1)a=−a(-1)a = -a and a(b−c)=ab−aca(b - c) = ab - ac).

[L4]

Coset equality is membership of a difference in the subgroup (x∈aHx\in aH iff a−1x∈Ha^{-1}x\in H, and aH=bHaH=bH iff a−1b∈Ha^{-1}b\in H).

[L5]

Additive cosets are available for an additive subgroup (The quotient group G/NG/N and coset product (gN)(hN)=ghN(gN)(hN)=ghN).

Proof

technique · direct
1.1

If JJ is an ideal and r′=r+ir'=r+i, s′=s+js'=s+j, then r′s′−rs=rj+is+ij∈Jr's'-rs=rj+is+ij\in J, so the product is well defined.

L1L2L3L4L5givenalgebra
2.1

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

step 1.1L1L2L3L4L5givenalgebra
3.1

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

step 2.1∎

Depends on

Used by

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: 25 results over 14 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