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 Thus the elementary divisors are and , while the invariant-factor list is the single entry .
Facts & Assumptions
Given: The objects and hypotheses in the example.
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).
For every finite abelian group there is a unique list such that . Moreover . The trivial group corresponds to the empty list and empty product. (Fundamental theorem of finite abelian groups: invariant-factor form).
Let be a finite pairwise-coprime list of positive integers and let . The map is a bijection. It preserves addition, multiplication, , and componentwise. For the empty list, 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).
For every , view as its canonical nonnegative integer and put . Then the left cosets of in are exactly the congruence classes modulo , and coset addition is the published addition of congruence classes. Thus as the same group on the same underlying set. This includes and . (For every , the congruence-class group is the quotient group ).
Verification
The residue map is an isomorphism by the Chinese remainder theorem.
The factors have prime-power orders, so is the elementary-divisor multiset; regrouping the coprime factors gives the invariant factor .
Depends on
- Fundamental theorem of finite abelian groups: elementary-divisor form
- Fundamental theorem of finite abelian groups: invariant-factor form
- 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
- For every $n\in\mathbb N$, the congruence-class group $(\mathbb Z/n,+)$ is the quotient group $(\mathbb Z,+)/n\mathbb Z$
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
- Keith Conrad, Decomposition of Finite Abelian Groups, §§1-4 (standard reference, not scraped)
- Richard Elman, Lectures on Abstract Algebra, Ch. 14 (standard reference, not scraped)