Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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 cyclic group of order six in elementary-divisor and invariant-factor forms

Example

The Chinese remainder isomorphism gives C6C2×C3.C_6\cong C_2\times C_3. Thus the elementary divisors are 22 and 33, while the invariant-factor list is the single entry 66.

Facts & Assumptions

Given: The objects and hypotheses in the example.

[L1]

Every finite abelian group is isomorphic to a finite direct product of cyclic groups of prime-power order. The multiset of their orders is uniquely determined by the group, up to permutation of the factors. (Fundamental theorem of finite abelian groups: elementary-divisor form).

[L2]

For every finite abelian group GG there is a unique list 1<n1nr1<n_1\mid\cdots\mid n_r such that GCn1××CnrG\cong C_{n_1}\times\cdots\times C_{n_r}. Moreover G=n1nr|G|=n_1\cdots n_r. The trivial group corresponds to the empty list and empty product. (Fundamental theorem of finite abelian groups: invariant-factor form).

[L3]

Let n0,,nr1n_0,\ldots,n_{r-1} be a finite pairwise-coprime list of positive integers and let N:=i<rniN:=\prod_{i<r}n_i. The map Φ:Z/Ni<rZ/ni,[x]N([x]ni)i<r,\Phi:\mathbb Z/N\longrightarrow\prod_{i<r}\mathbb Z/n_i,\qquad[x]_N\longmapsto([x]_{n_i})_{i<r}, is a bijection. It preserves addition, multiplication, [0][0], and [1][1] componentwise. For the empty list, N=1N=1 and both sides have one element. (Chinese remainder theorem for a finite pairwise-coprime list: simultaneous residues determine one class modulo the product, and the resulting bijection preserves addition and multiplication).

[L4]

For every nNn\in\mathbb N, view nn as its canonical nonnegative integer and put nZ:={nk:kZ}n\mathbb Z:=\{nk:k\in\mathbb Z\}. Then the left cosets of nZn\mathbb Z in (Z,+)(\mathbb Z,+) are exactly the congruence classes modulo nn, and coset addition is the published addition of congruence classes. Thus (Z,+)/nZ=(Z/n,+)(\mathbb Z,+)/n\mathbb Z=(\mathbb Z/n,+) as the same group on the same underlying set. This includes n=0n=0 and n=1n=1. (For every nNn\in\mathbb N, the congruence-class group (Z/n,+)(\mathbb Z/n,+) is the quotient group (Z,+)/nZ(\mathbb Z,+)/n\mathbb Z).

Verification

technique · direct
1.1

The residue map [x]6([x]2,[x]3)[x]_6\mapsto([x]_2,[x]_3) is an isomorphism by the Chinese remainder theorem.

givenL1L2L3L4
2.1

The factors C2,C3C_2,C_3 have prime-power orders, so {2,3}\{2,3\} is the elementary-divisor multiset; regrouping the coprime factors gives the invariant factor 66.

step 1.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: 97 results over 24 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