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.
In a cyclic group of order , has order
Statement
Let be cyclic of finite order . For every integer ,
Facts & Assumptions
Given: A generator of a cyclic group of order and an integer .
The order of an element is the least positive exponent giving the identity (The order of a finite group and the order of an element, with when no positive power of is the identity).
Since , one has exactly when (If then iff is an integer multiple of , the powers are distinct, and has exactly elements; if has infinite order then only for ).
for every integer (Exponent laws in a group: and for all , and when and commute).
Put ; then divides both and (Common divisor, and the greatest common divisor , with the convention ).
After dividing two integers by their nonzero greatest common divisor, the resulting quotients are coprime (If is nonzero then and are coprime).
If and , then (If and then ; and if , and then ).
Proof
Since , the common divisor is nonzero. Write and ; [L5] gives .
By [L2] and [L3], is equivalent to , hence to .
By [L6] and , the condition in step 2.1 is equivalent to .
Thus the least positive with is , which is the asserted order by [L1].
Depends on
- 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$
- 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**
- Common divisor, and the greatest common divisor $\gcd(a,b)$, with the convention $\gcd(0,0) := 0$
- If $d = \gcd(a,b)$ is nonzero then $a/d$ and $b/d$ are coprime
- If $\gcd(a,b) = 1$ and $a \mid bc$ then $a \mid c$; and if $a \mid c$, $b \mid c$ and $\gcd(a,b) = 1$ then $ab \mid c$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 82 results over 23 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
- Peter Hackman, Elementary Number Theory, §C.I (standard reference, not scraped)
- William Stein, Elementary Number Theory, §2.5 (standard reference, not scraped)