Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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\mathbb Z/n as a Z\mathbb Z-module

Example

For n≥1n\ge1, the additive group of residue classes Z/n\mathbb Z/n is a left Z\mathbb Z-module under

r [a]n:=[ra]n.r\,[a]_n:=[ra]_n.

Facts & Assumptions

Given: An integer n≥1n\ge1, a scalar r∈Zr\in\mathbb Z, and residue classes [a]n,[b]n∈Z/n[a]_n,[b]_n\in\mathbb Z/n.

[L1]

Addition and multiplication of residue classes are representative-independent (Addition and multiplication on Z/n\mathbb{Z}/n by [a]n+[b]n=[a+b]n[a]_n+[b]_n=[a+b]_n and [a]n[b]n=[ab]n[a]_n[b]_n=[ab]_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 nn, (Z/n,+)(\mathbb{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 aa by a congruent integer leaves rara congruent modulo nn.

L1L2given
2.1

Integer distributivity and associativity give r([a]n+[b]n)=r[a+b]n=[ra+rb]n=r[a]n+r[b]nr([a]_n+[b]_n)=r[a+b]_n=[ra+rb]_n=r[a]_n+r[b]_n, (r+s)[a]n=r[a]n+s[a]n(r+s)[a]_n=r[a]_n+s[a]_n, and (rs)[a]n=r(s[a]n)(rs)[a]_n=r(s[a]_n).

step 1.1L1L2given
3.1

Finally 1[a]n=[a]n1[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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 38 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