Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31
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 every natural nn, (Z/n,+)(\mathbb{Z}/n,+) is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold

Statement

For every n∈Nn\in\mathbb N, with addition and multiplication as in 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:

  1. (Z/n,+,[0]n)(\mathbb Z/n,+,[0]_n) is an abelian group (Group and abelian group), with −[a]n=[−a]n-[a]_n=[-a]_n;
  2. (Z/n,⋅,[1]n)(\mathbb Z/n,\cdot,[1]_n) is a commutative monoid (Semigroup and monoid);
  3. multiplication distributes over addition on both sides.

The assertions include n=0n=0 and n=1n=1. At n=1n=1, the two distinguished identities coincide because [0]1=[1]1[0]_1=[1]_1.

Facts & Assumptions

Given: A natural number nn and classes [a]n,[b]n,[c]n[a]_n,[b]_n,[c]_n in Z/n\mathbb Z/n.

[F1]

[u]n+[v]n=[u+v]n[u]_n+[v]_n=[u+v]_n and [u]n[v]n=[uv]n[u]_n[v]_n=[uv]_n, and these values are independent of representatives (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).

[L1]

Z\mathbb Z is a commutative ring: addition and multiplication are associative and commutative, 00 and 11 are identities, every integer has an additive inverse, and multiplication distributes over addition (The integers form a commutative ring).

[F2]

An abelian group is an associative commutative binary operation with an identity and inverses; a commutative monoid is an associative commutative binary operation with an identity (Group and abelian group, Semigroup and monoid).

Proof

technique · direct
1.1

Associativity and commutativity of addition follow from ([a]n+[b]n)+[c]n=[(a+b)+c]n=[a+(b+c)]n=[a]n+([b]n+[c]n)([a]_n+[b]_n)+[c]_n=[(a+b)+c]_n=[a+(b+c)]_n=[a]_n+([b]_n+[c]_n) and [a+b]n=[b+a]n[a+b]_n=[b+a]_n.

F1L1
1.2

The class [0]n[0]_n is an additive identity, and [−a]n[-a]_n is an additive inverse of [a]n[a]_n, since [a+0]n=[a]n[a+0]_n=[a]_n and [a+(−a)]n=[0]n[a+(-a)]_n=[0]_n.

F1L1
1.3

Associativity and commutativity of multiplication follow from [(ab)c]n=[a(bc)]n[(ab)c]_n=[a(bc)]_n and [ab]n=[ba]n[ab]_n=[ba]_n, while [1]n[1]_n is a multiplicative identity because [a⋅1]n=[a]n[a\cdot1]_n=[a]_n.

F1L1
1.4

Left distributivity is [a]n([b]n+[c]n)=[a(b+c)]n=[ab+ac]n=[a]n[b]n+[a]n[c]n[a]_n([b]_n+[c]_n)=[a(b+c)]_n=[ab+ac]_n=[a]_n[b]_n+[a]_n[c]_n; right distributivity follows identically, or from commutativity.

F1L1
2.1

Steps 1.1 and 1.2 verify the abelian-group clauses, step 1.3 verifies the commutative-monoid clauses, and step 1.4 gives both distributive laws.

step 1.1step 1.2step 1.3step 1.4F2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 35 results over 12 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