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.
Every cyclic group is isomorphic to or to for its finite order
Statement
If is cyclic, then exactly one of the following applies:
- if has infinite order, ;
- if has finite order , necessarily , then .
Facts & Assumptions
Given: A group and an element with .
A cyclic subgroup is precisely the set of all integer powers of its generator (, and every cyclic group is abelian).
For finite order , exactly when , while for infinite order no nonzero integer power of is the identity (If then iff is an integer multiple of , the powers are distinct, and has exactly elements; if has infinite order then only for ).
Integer powers satisfy and ; a bijective group homomorphism is a group isomorphism (Exponent laws in a group: and for all , and when and commute, Group isomorphisms, automorphisms and the set ).
The additive quotient group is the group (For every , the congruence-class group is the quotient group ).
Proof
Suppose first that has infinite order. The map , , is a homomorphism by the power law in [L3]. If , then by [L3], so [L2] forces ; it is surjective by [L1].
Suppose instead that has finite order . Then by the definition of element order, and defines a map because means , so [L2] gives and [L3] gives .
Hence in the infinite-order case is an isomorphism .
The map is a homomorphism by the power law, is injective because gives by [L3] and then [L2] gives , and is surjective by [L1].
Thus is an isomorphism in the finite-order case.
Steps 2.1 and 3.1 give the asserted classification according as the order of is infinite or finite.
Depends on
- The subgroup $\langle S \rangle$ generated by a subset, the cyclic subgroup $\langle g \rangle$, and cyclic groups
- $\langle g \rangle = \{\, g^{n} : n \in \mathbb{Z} \,\}$, and every cyclic group is abelian
- The order $|G|$ of a finite group and the order $\operatorname{ord}(g)$ of an element, with $\operatorname{ord}(g) = \infty$ when no positive power of $g$ is the identity
- If $\operatorname{ord}(g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$, the powers $g^{0}, \dots, g^{n-1}$ are distinct, and $\langle g \rangle$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$
- Monoid homomorphism and group homomorphism
- Exponent laws in a group: $g^{m+n} = g^{m}g^{n}$ and $(g^{m})^{n} = g^{mn}$ for all $m, n \in \mathbb{Z}$, and $(gh)^{n} = g^{n}h^{n}$ **when $g$ and $h$ commute**
- Group isomorphisms, automorphisms and the set $\operatorname{Aut}(G)$
- For every $n\in\mathbb N$, the congruence-class group $(\mathbb Z/n,+)$ is the quotient group $(\mathbb Z,+)/n\mathbb Z$
Used by
- A nontrivial finite abelian group is cyclic if and only if it has one invariant factor Corollary
- Elementary-divisor data for a finite abelian group Definition
- Invariant-factor data for a finite abelian group Definition
- Elementary divisors regroup uniquely into invariant factors Lemma
- Cauchy's theorem for finite abelian groups Theorem
- Every finite abelian p-group is a direct product of cyclic p-groups Theorem
- Fundamental theorem of finite abelian groups: elementary-divisor form Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 84 results over 25 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
- Romyar Sharifi, Abstract Algebra (standard reference, not scraped)