ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)

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.

For $n \geq 1$ the congruence classes modulo $n$ form an abelian group $(Z / n, +)$ of order $n$ , generated by the class of $1$

Example

Fix a natural number $n \geq 1$ and write $\overset{ˉ}{n} : = ι (n)$ for the corresponding positive integer, $ι : N \to Z$ being the embedding of The naturals embed in the integers. For $a, b \in Z$ define

$a \equiv b (m o d n) : ⟺ a - b = q \overset{ˉ}{n} for some q \in Z,$

that is, $\overset{ˉ}{n} ∣ (a - b)$ (Division with remainder in $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ ). Then:

$\equiv$ is an equivalence relation on $Z$ (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ); its classes are the congruence classes modulo $n$ , and the quotient set is written $Z / n$ ;
$[a] + [b] : = [a + b]$ is a well-defined binary operation on $Z / n$ , and $(Z / n, +, [0])$ is an abelian group (Group and abelian group);
$Z / n$ is finite of order $n$ : $∣ Z / n ∣ = n$ (The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity);
$Z / n = ⟨ [1] ⟩$ , so it is cyclic, generated by the class of $1$ (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

The hypothesis $n \geq 1$ is needed for claim 3, and for claim 3 only: at $n = 0$ the relation is equality, so $Z / 0$ has one class for each integer and is infinite, and there is no natural number $n$ with $∣ Z / 0 ∣ = n$ . Claims 1, 2 and 4 do hold at $n = 0$ , where $Z / 0$ is an infinite cyclic group generated by $[1]$ .

Facts & Assumptions

Given: A natural number $n \geq 1$ , the integer $\overset{ˉ}{n} = ι (n)$ , and the relation $a \equiv b$ meaning $a - b = q \overset{ˉ}{n}$ for some $q \in Z$ (The integers as equivalence classes of pairs of naturals, Arithmetic on the integers).

[L1]

$Z$ is a commutative ring, with $u - v : = u + (- v)$ (The integers form a commutative ring, Arithmetic on the integers); its order is total and antisymmetric and compatible with addition, and positives are closed under multiplication (The integers form a totally ordered ring, Order on the integers).

[L2]

$ι$ is injective, preserves addition, multiplication and order, and its image is exactly the nonnegative integers; $ι (0) = 0$ , $ι (1) = 1$ ; hence $\overset{ˉ}{n} > 0$ because $n \geq 1$ (The naturals embed in the integers, Order on the natural numbers, The natural numbers $N$ (von Neumann)). Moreover $n = {s \in N : s < n}$ : a natural number is exactly the set of the naturals below it (On $N$ the order is membership: $m < n ⟺ m \in n$ ).

[L3]

An equivalence relation is a reflexive, symmetric and transitive relation; $[a] = {b : a \sim b}$ and the quotient set is the set of classes (Equivalence relation, equivalence class, and the quotient set $A / \sim$ ); and $a \sim b$ if and only if $[a] = [b]$ (The equivalence classes of an equivalence relation are nonempty, cover $A$ , and are pairwise equal or disjoint; conversely every such cover arises from exactly one equivalence relation).

[L4]

Division with remainder: for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ (Division with remainder in $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ ).

[L5]

A group is a monoid all of whose elements are invertible; abelian means commutative; the order $∣ G ∣$ of a finite group is the unique natural $m$ with $G \approx m$ ; $⟨ g ⟩$ is the smallest subgroup containing $g$ and equals the set of integer powers of $g$ (Group and abelian group, Binary operation on a set; associativity, commutativity, and a subset closed under the operation, Left identity, right identity, and two-sided identity for a binary operation, The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity, The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups, $⟨ g ⟩ = {g^{n} : n \in Z}$ , and every cyclic group is abelian, Finite, countably infinite, countable, uncountable, Equinumerous sets, $A \approx B$ and $A ⪯ B$ , Injection, surjection, bijection).

[L6]

Powers in a group written additively: $g^{0}$ is the identity, $g^{σ (m)} = g^{m} + g$ , and $g^{x} = - g^{k}$ when $x < 0$ and $- x = ι (k)$ (Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ ).

[L7]

Induction on $N$ (The principle of mathematical induction); on $N$ exactly one of $s < t$ , $s = t$ , $t < s$ holds (Trichotomy of the order on $N$ ).

Verification

technique · direct

1.1

$\equiv$ is reflexive, since $a - a = 0 = 0 \cdot \overset{ˉ}{n}$ ; symmetric, since $a - b = q \overset{ˉ}{n}$ gives $b - a = (- q) \overset{ˉ}{n}$ ; and transitive, since $a - b = q \overset{ˉ}{n}$ and $b - c = q^{'} \overset{ˉ}{n}$ give $a - c = (a - b) + (b - c) = (q + q^{'}) \overset{ˉ}{n}$ . So it is an equivalence relation, and $Z / n$ is its quotient set.

L1L3

1.2

The operation is well defined: if $a \equiv a^{'}$ and $b \equiv b^{'}$ , say $a - a^{'} = q \overset{ˉ}{n}$ and $b - b^{'} = q^{'} \overset{ˉ}{n}$ , then $(a + b) - (a^{'} + b^{'}) = (a - a^{'}) + (b - b^{'}) = (q + q^{'}) \overset{ˉ}{n}$ , so $a + b \equiv a^{'} + b^{'}$ and $[a + b] = [a^{'} + b^{'}]$ . Hence $[a] + [b] : = [a + b]$ depends only on the classes.

L1L3

1.3

$ι$ reflects the order: if $ι (s) < ι (t)$ then $s < t$ , since otherwise $t \leq s$ would give $ι (t) \leq ι (s)$ , contradicting antisymmetry.

L1L2L7

1.4

Distinct such representatives give distinct classes: let $s, t \in N$ with $s < n$ , $t < n$ and $[ι (s)] = [ι (t)]$ , so $ι (s) - ι (t) = q \overset{ˉ}{n}$ for some $q$ , that is $ι (s) = q \overset{ˉ}{n} + ι (t)$ . Both $ι (s)$ and $ι (t)$ are nonnegative and, $ι$ preserving the order, both are $< ι (n) = \overset{ˉ}{n}$ . So $ι (s)$ is written as $q \overset{ˉ}{n} + ι (t)$ with $0 \leq ι (t) < \overset{ˉ}{n}$ and also as $0 \cdot \overset{ˉ}{n} + ι (s)$ with $0 \leq ι (s) < \overset{ˉ}{n}$ ; the uniqueness clause of division with remainder forces $q = 0$ and $ι (t) = ι (s)$ , whence $s = t$ by injectivity of $ι$ .

L1L2L3L4

1.5

In the group $Z / n$ the $k$ -th power of $[1]$ in additive notation is $[ι (k)]$ for every $k \in N$ : the set of $k$ for which this holds contains $0$ , since the identity is $[0] = [ι (0)]$ , and is closed under $σ$ , since the power at $σ (k)$ is the power at $k$ plus $[1]$ , that is $[ι (k)] + [1] = [ι (k) + 1] = [ι (σ (k))]$ .

L1L2L6L7

2.1

$(Z / n, +, [0])$ is an abelian group: associativity, commutativity, the identity law $[a] + [0] = [a + 0] = [a]$ and the inverse law $[a] + [- a] = [0]$ all follow from the corresponding identities in $Z$ applied to representatives, which is legitimate by step 1.2.

step 1.2L1L5

2.2

Every class has a representative $r$ with $0 \leq r < \overset{ˉ}{n}$ : given $a$ , divide $a = q \overset{ˉ}{n} + r$ with $0 \leq r < \overset{ˉ}{n}$ , so $a - r = q \overset{ˉ}{n}$ and $[a] = [r]$ . Moreover $r \geq 0$ gives $r = ι (s)$ for a unique $s \in N$ , and $ι (s) < ι (n)$ gives $s < n$ .

step 1.3L2L3L4

3.1

The map $φ : n \to Z / n$ with $φ (s) = [ι (s)]$ is well defined, the elements of the natural number $n$ being exactly the naturals $s < n$ ; it is surjective by step 2.2 and injective by step 1.4, hence a bijection. So $Z / n \approx n$ and $∣ Z / n ∣ = n$ .

step 2.2step 1.4L2L5

3.2

For a negative integer $x$ with $- x = ι (k)$ , the $x$ -th power of $[1]$ is the inverse of $[ι (k)]$ , namely $[- ι (k)] = [x]$ ; with step 1.5 this gives that the set of integer powers of $[1]$ is ${[a] : a \in Z} = Z / n$ .

step 2.1step 1.5L1L2L6

4.1

Since $⟨ [1] ⟩$ is exactly the set of integer powers of $[1]$ , step 3.2 gives $⟨ [1] ⟩ = Z / n$ , so $Z / n$ is cyclic, generated by $[1]$ .

step 3.2L5

5.1

Claims 1 to 4 are established in steps 1.1, 2.1, 3.1 and 4.1.

step 1.1step 2.1step 3.1step 4.1∎

Remarks

The hypothesis $n \geq 1$ is carried by the title and by the statement, not left implicit. It is used twice and in an essential way: $\overset{ˉ}{n} > 0$ is what makes Division with remainder in $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ applicable in step 2.2, and it is what makes the count in step 3.1 come out as $n$ . At $n = 0$ the relation $\equiv$ is equality on $Z$ , the quotient set is in bijection with $Z$ itself, and the group is infinite.
No greatest common divisor is used anywhere above, and none is available at this point in the reading order. Only division with remainder is needed. The multiplicative structure of $Z / n$ , where the units are the classes coprime to $n$ , does need gcd theory and belongs to a later page.
The elements are congruence classes, that is subsets of $Z$ , and $[a]$ is a set. Nothing above ever names an element of $Z / n$ except through a representative, which is why step 1.2 has to be checked before the operation may be written down at all.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

71 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

Modular arithmetic (Wikipedia) (standard reference, not scraped)
Cyclic group (Wikipedia) (standard reference, not scraped)

For n≥1n≥1 the congruence classes modulo nn form an abelian group (Z/n,+)(Z/n,+) of order nn, generated by the class of 11