ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03

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 residue classes $Z / n$ as a $Z$ -module

Example

For $n \geq 1$ , the additive group of residue classes $Z / n$ is a left $Z$ -module under

$r [a]_{n} : = [r a]_{n} .$

Facts & Assumptions

Given: An integer $n \geq 1$ , a scalar $r \in Z$ , and residue classes $[a]_{n}, [b]_{n} \in Z / n$ .

[L1]

Addition and multiplication of residue classes are representative-independent (Addition and multiplication on $Z / n$ by $[a]_{n} + [b]_{n} = [a + b]_{n}$ and $[a]_{n} [b]_{n} = [a b]_{n}$ ).

[L2]

The integers form a commutative ring (The integers form a commutative ring).

[L3]

The additive residue classes form an abelian group (For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

[L4]

A left module is an abelian group with a unital distributive associative scalar action (Unital left and right modules over a ring; unqualified module means left module).

Verification

technique · direct

1.1

The displayed action is representative-independent: replacing $a$ by a congruent integer leaves $r a$ congruent modulo $n$ .

L1L2given

2.1

Integer distributivity and associativity give $r ([a]_{n} + [b]_{n}) = r [a + b]_{n} = [r a + r b]_{n} = r [a]_{n} + r [b]_{n}$ , $(r + s) [a]_{n} = r [a]_{n} + s [a]_{n}$ , and $(r s) [a]_{n} = r (s [a]_{n})$ .

step 1.1L1L2given

3.1

Finally $1 [a]_{n} = [a]_{n}$ , and [L3] supplies the abelian additive group; therefore the module axioms hold.

step 2.1L1L2L3L4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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

McGerty, Algebra II: Rings and Modules, Section 3 (standard reference, not scraped)

The residue classes Z/nZ/n as a ZZ-module