LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-28

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.

Cancellation characterises domains: in a commutative ring with $1 \ne 0$ , the implication $ab = ac$ and $a \ne 0$ imply $b = c$ holds if and only if the ring has no zero divisors

Statement

Let $R$ be a commutative ring (Commutative ring) with $1 \ne 0$ . Consider the two conditions

(C) for all $a, b, c \in R$ : if $ab = ac$ and $a \ne 0$ then $b = c$ ;
(Z) $R$ has no zero divisors (Zero divisor, and integral domain: a commutative ring with $1 \ne 0$ and no zero divisors).

Then (C) holds if and only if (Z) holds; that is, (C) holds exactly when $R$ is an integral domain.

Facts & Assumptions

Given: A commutative ring $R$ with zero $0$ and identity $1$ , and $1 \ne 0$ (Commutative ring, Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides).

[L1]

$(R,+,0)$ is an abelian group and multiplication is commutative and distributes over addition (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides, Commutative ring, Group and abelian group).

[L2]

$a(b - c) = ab - ac$ and $a \cdot 0 = 0 = 0 \cdot a$ for all $a, b, c \in R$ (In any ring $0 \cdot a = a \cdot 0 = 0$ , $(-a)b = a(-b) = -(ab)$ , $(-a)(-b) = ab$ , $(-1)a = -a$ and $a(b - c) = ab - ac$ ).

[L3]

Cancellation in the additive group: $x + z = y + z$ implies $x = y$ (Cancellation in a group: $gx = gy$ or $xg = yg$ forces $x = y$ ; equivalently left and right translation by $g$ are bijections of $G$ , so $gx = h$ and $xg = h$ each have exactly one solution, Group and abelian group).

[L4]

$a$ is a zero divisor when $a \ne 0$ and $ab = 0$ for some $b \ne 0$ ; $R$ has no zero divisors exactly when $ab = 0$ implies $a = 0$ or $b = 0$ ; and an integral domain is exactly a commutative ring with $1\ne0$ and no zero divisors (Zero divisor, and integral domain: a commutative ring with $1 \ne 0$ and no zero divisors).

Proof

technique · direct

1.1

Assume (Z), and let $ab = ac$ with $a \ne 0$ . Then $a(b - c) = ab - ac = 0$ .

L2given

1.2

Assume (C), and let $ab = 0$ with $a \ne 0$ . Then $ab = 0 = a \cdot 0$ .

L2given

2.1

From step 1.1, (Z) gives $a = 0$ or $b - c = 0$ ; since $a \ne 0$ , we get $b + (-c) = 0$ . As also $c + (-c) = 0$ , cancelling $-c$ gives $b = c$ . So (Z) implies (C).

step 1.1L1L3L4

2.2

From step 1.2, (C) applied with $a$ , $b$ and $0$ gives $b = 0$ . So whenever $ab = 0$ and $a \ne 0$ we have $b = 0$ , which says exactly that $ab = 0$ implies $a = 0$ or $b = 0$ ; hence (Z). So (C) implies (Z).

step 1.2L4

3.1

By steps 2.1 and 2.2 the two conditions are equivalent, and (Z) together with commutativity and $1 \ne 0$ is the definition of an integral domain.

step 2.1step 2.2L4∎

Remarks

The hypothesis $1 \ne 0$ is used nowhere in the equivalence itself. It is carried in the statement only so that "(C) holds exactly when $R$ is an integral domain" is literally true, since (D1) of Zero divisor, and integral domain: a commutative ring with $1 \ne 0$ and no zero divisors is part of being a domain. In the one-element ring both (C) and (Z) hold vacuously and the ring is still not a domain.
Cancellation is by $a$ , not by $0$ . The clause $a \ne 0$ cannot be dropped: $0 \cdot b = 0 \cdot c$ holds for all $b$ and $c$ in every ring (In any ring $0 \cdot a = a \cdot 0 = 0$ , $(-a)b = a(-b) = -(ab)$ , $(-a)(-b) = ab$ , $(-1)a = -a$ and $a(b - c) = ab - ac$ ), so cancelling $0$ would collapse the ring.
Multiplicative cancellation does not make the nonzero elements a group. It makes $(R \setminus \{0\}, \cdot, 1)$ a cancellative commutative monoid, and $\mathbb{Z}$ shows that is strictly weaker than being a group: $2$ cancels and is not invertible. The rings where the nonzero elements do form a group are the fields (Every commutative division ring is a field, so "field" and "commutative division ring" name the same structures and the published definition and the ring-theoretic one agree).

Depends on

Used by

Every prime element of an integral domain is irreducible Lemma

Dependency tree · next 3 levels

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

Integral domain (Wikipedia) (standard reference, not scraped)
Cancellation property (Wikipedia) (standard reference, not scraped)
Thomas W. Judson, Abstract Algebra: Theory and Applications, §16.4: Integral Domains and Fields (standard reference, not scraped)

Cancellation characterises domains: in a commutative ring with 1≠01 \ne 01=0, the implication ab=acab = acab=ac and a≠0a \ne 0a=0 imply b=cb = cb=c holds if and only if the ring has no zero divisors