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.

The sum and product of two-sided ideals are two-sided ideals

Statement

The sum and product of two-sided ideals are two-sided ideals.

Facts & Assumptions

Given: Two-sided ideals I,J⊴RI,J\mathrel{\trianglelefteq}R.

[L1]

I+JI+J and IJIJ are the indicated elementwise and finite-sum sets (The sum I+JI+J and product IJIJ of two-sided ideals).

[L2]

The ideal criterion is subtraction closure plus two-sided absorption (Ideal criteria and intersections of ideals).

[L3]

Ring multiplication distributes over finite sums (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).

Proof

technique · direct
1.1

Subtraction closure of I+JI+J and of IJIJ follows by subtracting representatives and concatenating finite sums.

L1L2L3givenalgebra
2.1

Multiplying a representative on either side keeps it in I+JI+J, and distributivity keeps each summand of a product in IJIJ.

step 1.1L1L2L3givenalgebra
3.1

The closure established in step 2.1 proves both claims.

step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 17 results over 11 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