ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

$(\mathbb{Z}, +)$ is an abelian group, $(\mathbb{Z}, \cdot)$ is a commutative monoid that is not a group, and its group of units is $\{1, -1\}$

Example

Let $\mathbb{Z}$ be the integers with the operations of Arithmetic on the integers. Then

$(\mathbb{Z}, +, 0)$ is an abelian group (Group and abelian group);
$(\mathbb{Z}, \cdot, 1)$ is a commutative monoid (Semigroup and monoid) which is not a group, because $0$ has no multiplicative inverse;
its group of units (The invertible elements of a monoid form a group under the restricted operation) is $\mathbb{Z}^{\times} = \{1, -1\}$ , and $1 \ne -1$ .

Facts & Assumptions

Given: The integers $\mathbb{Z}$ with $+$ , $\cdot$ , $0$ and $1$ (The integers as equivalence classes of pairs of naturals, Arithmetic on the integers), and the embedding $\iota : \mathbb{N} \to \mathbb{Z}$ of The naturals embed in the integers.

[L1]

In $\mathbb{Z}$ : addition is associative and commutative, $x + 0 = x$ , and every $x = [(a,b)]$ has the additive inverse $-x = [(b,a)]$ with $x + (-x) = 0$ ; multiplication is associative and commutative with $x \cdot 1 = x$ , and it distributes over addition. These are the ring axioms, verified one by one in the proof of The integers form a commutative ring (The integers form a commutative ring, Arithmetic on the integers).

[L2]

The order on $\mathbb{Z}$ is total, antisymmetric and transitive, is compatible with addition, and positives are closed under multiplication (The integers form a totally ordered ring, Order on the integers).

[L3]

$\iota$ is injective, preserves addition, multiplication and order, and its image is exactly the nonnegative integers; $\iota(0) = 0$ and $\iota(1) = 1$ (The naturals embed in the integers).

[L4]

On $\mathbb{N}$ : every $k \ne 0$ is a successor $\sigma(j) = 1 + j$ , so $k \ne 0$ implies $1 \le k$ (Every nonzero natural number is a successor, Addition is commutative, Order on the natural numbers, The natural numbers $\mathbb{N}$ (von Neumann)).

[L5]

A group is a monoid in which every element is invertible; the units of a monoid form a group (Group and abelian group, Semigroup and monoid, Left inverse, right inverse, and invertible element of a monoid, Left identity, right identity, and two-sided identity for a binary operation, The invertible elements of a monoid form a group under the restricted operation).

Verification

technique · direct

1.1

Addition on $\mathbb{Z}$ is associative and commutative, $x + 0 = x$ and hence $0 + x = x$ , and every $x$ has a two-sided additive inverse $-x$ ; so $(\mathbb{Z},+,0)$ is an abelian group.

L1L5

1.2

Multiplication on $\mathbb{Z}$ is associative and commutative and $x \cdot 1 = x = 1 \cdot x$ ; so $(\mathbb{Z},\cdot,1)$ is a commutative monoid.

L1L5

1.3

For every $y \in \mathbb{Z}$ , $0 \cdot y = 0$ : by distributivity $0 \cdot y = (0+0) \cdot y = 0 \cdot y + 0 \cdot y$ , and adding $-(0 \cdot y)$ gives $0 = 0 \cdot y$ .

1.4

$1 \ne 0$ in $\mathbb{Z}$ : $\iota$ is injective with $\iota(1) = 1$ and $\iota(0) = 0$ , and $1 \ne 0$ in $\mathbb{N}$ since $1 = \sigma(0)$ contains $0$ as an element while $0 = \varnothing$ has none.

L3L4

1.5

Discreteness in $\mathbb{Z}$ : if $0 < x$ then $1 \le x$ . Indeed $x \ge 0$ gives $x = \iota(k)$ with $k \in \mathbb{N}$ , and $k \ne 0$ since $\iota(0) = 0 \ne x$ ; so $1 \le k$ in $\mathbb{N}$ and, $\iota$ preserving the order, $1 = \iota(1) \le \iota(k) = x$ .

L3L4

2.1

$0$ is not invertible in $(\mathbb{Z},\cdot,1)$ : $0 \cdot y = 0 \ne 1$ for every $y$ . Hence $(\mathbb{Z},\cdot,1)$ is not a group.

step 1.3step 1.4L5

2.2

$1$ and $-1$ are units: $1 \cdot 1 = 1$ , and $(-1)(-1) = 1$ because $(-1)(-1) + (-1) = (-1)\bigl((-1) + 1\bigr) = (-1) \cdot 0 = 0$ , so $(-1)(-1)$ is the additive inverse of $-1$ , which is $1$ .

step 1.3L1

2.3

If $0 < u$ and $1 \le v$ then $u \le uv$ : from $1 \le v$ we get $0 \le v - 1$ , so $u(v-1) \ge 0$ , either factor being possibly zero, and $uv - u = u(v-1) \ge 0$ gives $u \le uv$ .

step 1.5L1L2

2.4

Let $xy = 1$ . Then $x \ne 0$ and $y \ne 0$ by step 1.3 and step 1.4. If $x > 0$ and $y < 0$ then $0 < x(-y) = -(xy) = -1$ , so $1 < 0$ , contradicting $0 < 1$ , which holds by step 1.4 and totality since $1 \ge 0$ ; the case $x < 0$ , $y > 0$ is the same with the names interchanged. So $x$ and $y$ are both positive or both negative.

step 1.3step 1.4L1L2L3

3.1

Both positive: $1 \le x$ and $1 \le y$ by step 1.5, so $x \le xy = 1$ by step 2.3, and with $1 \le x$ antisymmetry gives $x = 1$ .

step 1.5step 2.3L2

4.1

Both negative: then $0 < -x$ and $0 < -y$ and $(-x)(-y) = xy = 1$ by ring arithmetic, so $-x = 1$ by step 3.1, that is $x = -1$ .

step 3.1L1L2

5.1

By steps 2.2, 2.4, 3.1 and 4.1 the units of $(\mathbb{Z},\cdot,1)$ are exactly $1$ and $-1$ ; and $1 \ne -1$ , since $1 = -1$ would give $1 + 1 = 0$ , while $0 < 1$ gives $1 < 1 + 1$ and hence $0 < 1 + 1$ . So $\mathbb{Z}^{\times} = \{1,-1\}$ , a group under multiplication with two elements.

step 2.2step 2.4step 3.1step 4.1L1L2L5∎

Remarks

The Statement of The integers form a commutative ring is quoted here by its content, not by its name. That theorem says $\mathbb{Z}$ is "a commutative ring with multiplicative identity", a phrase not defined at this point in the reading order; what is used above is the list of equations its proof verifies one at a time. Nothing here presupposes a definition of a ring.
Cancellation without invertibility. $(\mathbb{Z},\cdot)$ satisfies cancellation by nonzero elements yet is not a group, and $(\mathbb{N},+)$ is a sharper example still, being cancellative outright (A commutative monoid in which cancellation holds need not be a group: $(\mathbb{N}, +)$ ).
$\mathbb{Z}^{\times} = \{1,-1\}$ is the first finite group in the library that is not trivial. It is cyclic of order $2$ , generated by $-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: 53 results over 17 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

Integer (Wikipedia) (standard reference, not scraped)
Unit (ring theory) (Wikipedia) (standard reference, not scraped)

(Z,+)(\mathbb{Z}, +)(Z,+) is an abelian group, (Z,⋅)(\mathbb{Z}, \cdot)(Z,⋅) is a commutative monoid that is not a group, and its group of units is {1,−1}\{1, -1\}{1,−1}