artin_primitive_roots.variants.part_ii_square_or_minus_one

**Artin's Conjecture on Primitive Roots**, second half, different residue version If $a$ is a square number or $a = −1$, then the density of the set $S(a)$ of primes $p$ such that $a$ is a primitive root modulo $p$ is $0$.

theorem artin_primitive_roots.variants.part_ii_square_or_minus_one
    (a : ℤ) (ha : IsSquare a ∨ a = -1) :
    (S a).HasDensity 0 {p | p.Prime}

Recent Submissions

No submissions yet. Be the first to attempt this problem.