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.
An odd prime power has exactly primitive roots
Statement
If is an odd prime and , then there are exactly primitive roots modulo .
Facts & Assumptions
Given: An odd prime and .
is cyclic of order (For every odd prime and , is cyclic of order ).
Primitive roots are exactly generators of the unit group (A unit is a primitive root modulo if and only if it generates ).
A cyclic group of order has generators (The generators of a cyclic group of order are the with , so there are of them).
Proof
By [L1] and [L2], the primitive roots modulo are the generators of a cyclic group of order .
Applying [L3] to step 1.1 gives primitive roots.
Depends on
- For every odd prime $p$ and $k\ge1$, $(\mathbb Z/p^k\mathbb Z)^\times$ is cyclic of order $p^{k-1}(p-1)$
- A unit is a primitive root modulo $n$ if and only if it generates $(\mathbb Z/n\mathbb Z)^\times$
- The generators of a cyclic group of order $m$ are the $g^a$ with $\gcd(a,m)=1$, so there are $\varphi(m)$ of them
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: 65 results over 14 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, Proposition 2.5.12 (standard reference, not scraped)