ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 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.

The zero ring ${0}$ , in which $1 = 0$ : a commutative ring of characteristic $1$ that is not a domain, not a division ring and not a field

Example

Let $Z = {z}$ be a one-element set, and define $z + z : = z$ , $z \cdot z : = z$ , $0_{Z} : = z$ and $1_{Z} : = z$ . Then:

$Z$ is a commutative ring (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides, Commutative ring), the zero ring, and $1_{Z} = 0_{Z}$ ;
up to the choice of the single element, it is the only ring in which $1 = 0$ : any ring $R$ with $1_{R} = 0_{R}$ has $R = {0_{R}}$ (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$ );
$Z$ has no zero divisors, and is nevertheless not an integral domain (Zero divisor, and integral domain: a commutative ring with $1 \neq 0$ and no zero divisors), because it fails $1 \neq 0$ ;
$Z$ is not a division ring (Division ring: a ring with $1 \neq 0$ in which every nonzero element is a unit) and not a field (Field), for the same reason;
$char (Z) = 1$ (The characteristic of a ring: the least $n \geq 1$ with $n \cdot 1_{R} = 0$ when one exists, and $0$ otherwise).

Facts & Assumptions

Given: The one-element set $Z = {z}$ with $z + z = z$ , $z \cdot z = z$ , $0_{Z} = z$ and $1_{Z} = z$ .

[L1]

A ring is an abelian group under addition, a monoid under multiplication, and satisfies both distributive laws; it is commutative when its multiplication is (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides, Commutative ring).

[L2]

In a ring with $1 = 0$ , every element equals $0$ ; so such a ring has exactly one element (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$ ).

[L3]

An integral domain is a commutative ring with $1 \neq 0$ and no zero divisors; an element $a$ is a zero divisor only if $a \neq 0$ (Zero divisor, and integral domain: a commutative ring with $1 \neq 0$ and no zero divisors).

[L4]

A division ring is a ring with $1 \neq 0$ in which every nonzero element is a unit; a field has $0 \neq 1$ among its axioms (Division ring: a ring with $1 \neq 0$ in which every nonzero element is a unit, Field).

[L5]

$char (R)$ is the least $n \in N$ with $n \geq 1$ and $n \cdot 1_{R} = 0_{R}$ , if there is one, and $0$ otherwise; the multiples satisfy $0 \cdot a = 0_{R}$ and $σ (n) \cdot a = n \cdot a + a$ (The characteristic of a ring: the least $n \geq 1$ with $n \cdot 1_{R} = 0$ when one exists, and $0$ otherwise, Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ ).

Verification

technique · direct

1.1

Every equation between elements of $Z$ holds, since $Z$ has exactly one element and both sides of any equation are that element. In particular addition is associative and commutative with two-sided identity $0_{Z}$ and with $z$ its own additive inverse; multiplication is associative and commutative with two-sided identity $1_{Z}$ ; and both distributive laws hold. So $Z$ is a commutative ring, and $1_{Z} = z = 0_{Z}$ . This is claim 1.

L1given

1.2

Claim 2 is [L2]: if $R$ is a ring with $1_{R} = 0_{R}$ then $x = 1_{R} x = 0_{R} x = 0_{R}$ for every $x \in R$ , so $R = {0_{R}}$ .

1.3

$Z$ has no zero divisors: a zero divisor must be an element $a \neq 0$ , and $Z$ has no such element.

L3given

2.1

Claim 3: by step 1.1 the ring $Z$ is commutative, by step 1.3 it has no zero divisors, and by step 1.1 it has $1_{Z} = 0_{Z}$ ; the clause $1 \neq 0$ of [L3] therefore fails and $Z$ is not an integral domain.

step 1.1step 1.3L3

2.2

Claim 4: the clause $1 \neq 0$ of [L4] fails in $Z$ , so $Z$ is not a division ring; and the axioms of Field require $0 \neq 1$ , so $Z$ is not a field. Note that "every nonzero element is a unit" holds vacuously in $Z$ , so it is only the clause $1 \neq 0$ that excludes it from being a division ring.

step 1.1L4

2.3

$1 \cdot 1_{Z} = 0 \cdot 1_{Z} + 1_{Z} = 0_{Z} + 1_{Z} = 1_{Z} = 0_{Z}$ , using the recursion of [L5] at $σ (0) = 1$ and $1_{Z} = 0_{Z}$ from step 1.1.

step 1.1L5

3.1

Claim 5: by step 2.3 the natural number $1$ satisfies $1 \geq 1$ and $1 \cdot 1_{Z} = 0_{Z}$ , and no natural number $n$ with $n \geq 1$ is smaller than $1$ ; so the least such $n$ is $1$ and $char (Z) = 1$ .

step 2.3L5∎

Remarks

This is the item that makes $1 \neq 0$ a visible hypothesis. Zero divisor, and integral domain: a commutative ring with $1 \neq 0$ and no zero divisors, Division ring: a ring with $1 \neq 0$ in which every nonzero element is a unit and Field each carry that clause, and the zero ring is what each of them excludes. It satisfies every other clause of the first two: it is a commutative ring, it has no zero divisors, and every nonzero element of it is vacuously a unit. For Field the clause $0 \neq 1$ is not the only one that fails, and this is worth saying rather than glossing: axiom (M) there asks that $F ∖ {0}$ be an abelian group with identity $1$ , and in the zero ring that set is empty, so it has no identity at all. The two failures are the same phenomenon, since $1 = 0$ is exactly what empties $F ∖ {0}$ .
Characteristic $1$ occurs exactly here. By claim 2 a ring has $1 = 0$ only if it is the zero ring, and by The characteristic of a ring: the least $n \geq 1$ with $n \cdot 1_{R} = 0$ when one exists, and $0$ otherwise the characteristic is $1$ exactly when $1 \cdot 1_{R} = 1_{R} = 0_{R}$ . So the zero ring is the only ring of characteristic $1$ , and every other ring has characteristic $0$ or a characteristic that is at least $2$ .
The zero ring is not excluded from being a ring. Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides does not require $1 \neq 0$ , deliberately. The ring of all functions from the empty set into a ring has exactly one element, the empty function (The ring $R^{X}$ of all functions from a set $X$ into a ring, with pointwise operations), so it is the zero ring; requiring $1 \neq 0$ in the definition of a ring would make that construction partial.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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

Zero ring (Wikipedia) (standard reference, not scraped)
Thomas W. Judson, Abstract Algebra: Theory and Applications, §16.3: Rings (standard reference, not scraped)

The zero ring {0}{0}, in which 1=01=0: a commutative ring of characteristic 11 that is not a domain, not a division ring and not a field