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.
A direct product of two finite cyclic groups is cyclic if and only if their orders are coprime
Statement
If and are finite cyclic groups of orders , then is cyclic if and only if .
Facts & Assumptions
Given: Cyclic groups and .
The external direct product uses componentwise multiplication (The external direct product with componentwise multiplication) and is a group ( is a group with identity , coordinatewise inverses, and homomorphic coordinate projections).
A power of an element of order is the identity exactly when its exponent is divisible by (If then iff is an integer multiple of , the powers are distinct, and has exactly elements; if has infinite order then only for ).
is the least positive common multiple of and (Common multiple, and the least common multiple , taken to be when or ).
For positive integers , (Every common multiple of and is a multiple of , and ).
Proof
For with coordinate orders and , [L1] and [L2] show that exactly when both and ; its order is therefore by [L3].
If , [L4] and step 1.1 give , so generates the product of order .
Conversely, if the product is cyclic, a generator has order . Its coordinate orders divide and , so step 1.1 gives ; hence , and [L4] gives .
Depends on
- The external direct product $G\times H$ with componentwise multiplication
- $G\times H$ is a group with identity $(e_G,e_H)$, coordinatewise inverses, and homomorphic coordinate projections
- 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$
- Common multiple, and the least common multiple $\operatorname{lcm}(a,b)$, taken to be $0$ when $a = 0$ or $b = 0$
- Every common multiple of $a$ and $b$ is a multiple of $\operatorname{lcm}(a,b)$, and $\gcd(a,b) \cdot \operatorname{lcm}(a,b) = |ab|$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 83 results over 22 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
- William Stein, Elementary Number Theory, Lemma 2.5.7 (standard reference, not scraped)