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.
Euler's criterion: if has a primitive root, , and , then is solvable if and only if
Statement
Let admit a primitive root, let , and let . Put . Then
is solvable if and only if
Facts & Assumptions
Given: Integers , , and satisfying the stated hypotheses, and .
A primitive root has order (Primitive roots modulo ).
Relative to a primitive root , every unit has a unique index modulo (The index of a unit relative to a primitive root).
Index calculus turns a power into scalar multiplication of its index (Index calculus: products become sums and powers become scalar multiples modulo ).
The congruence is solvable exactly when (For , is solvable exactly when , and then has exactly solution classes modulo ).
A greatest common divisor divides both of its arguments (Common divisor, and the greatest common divisor , with the convention ).
A class modulo is a unit exactly when its representative is coprime to (For , is a unit if and only if ).
Proof
Choose a primitive root , put , and let . By [L6], is a unit. If , then , so every solution is also a unit.
Again by [L1] and [L3], exactly when . Since by [L5], this is equivalent to .
By [L2] and [L3], writing a candidate unit as turns in the unit group into . By [L4], this is solvable exactly when .
Steps 2.1 and 1.2 give the claimed biconditional. The argument also covers and , where .
Depends on
- Primitive roots modulo $n$
- The index $\operatorname{ind}_g(a)$ of a unit relative to a primitive root
- Index calculus: products become sums and powers become scalar multiples modulo $\varphi(n)$
- For $n\ge1$, $ax\equiv b\pmod n$ is solvable exactly when $\gcd(a,n)\mid b$, and then has exactly $\gcd(a,n)$ solution classes modulo $n$
- Common divisor, and the greatest common divisor $\gcd(a,b)$, with the convention $\gcd(0,0) := 0$
- For $n\ge1$, $[a]_n$ is a unit if and only if $\gcd(a,n)=1$
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: 71 results over 16 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, Theorem C.III.1 (standard reference, not scraped)