ArtinPrimitiveRootsConjecture.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

16 declarations, 9 contain sorry, 0 declared as axioms

Artin's conjecture on primitive roots

Artin's conjecture predicts, given an integer $a$, densities of primes $p$ for which $a$ is a primitive root modulo $p$. Under certain conditions (when $a$ is not a power and its squarefree part is not $1\pmod{4}$) the density is given by Artin's constant $$\prod_{p\ \text{prime}} \left(1 - \frac{1}{p(p - 1)}\right).$$ For more general values of $a$, this constant must be corrected by certain factors.

When $a = b^m$, $m$ is a maximal odd power, the squarefree part of $b$ satisfies $b_0 \not\equiv 1\pmod{4}$. Then Artin's constant should be multiplied by $$\prod_{p \mid m} \frac{p(p - 2)}{p^2 - p - 1}.$$
When $a = b^m$, $m$ is a maximal power, the squarefree part of $b$ satisfies $b_0\equiv 1\pmod{4}$. Then Artin's constant should be multiplied by the factor in the above bullet, as well as an additional entanglement factor from the primes dividing $\gcd(b_0, m)$ and primes dividing $b_0$: $$1 - \prod_{p \mid \gcd(b_0, m)} \frac{1}{2 - p} \prod_{p \mid b_0, p\nmid m} \frac{1}{1 + p - p^2}.$$
When $a = -1$ or $a$ is a square, then the density is $0$.

Note that Artin's conjecture has been proved by Hooley [Ho67] subject to the Riemann hypothesis for the Dedekind zeta functions of the Kummer fields $\mathbb{Q}(\zeta_k, a^{1/k})$, $k$ squarefree. These fields are in general non-abelian over $\mathbb{Q}$, so this hypothesis is not covered by the Generalized Riemann Hypothesis for Dirichlet $L$-functions.

References:

Wikipedia
A85397
LMS14 Lenstra, H.W. et al. "Character sums for primitive root densities" arXiv:1112.4816 [math.NT] (2014).
[Ho67] Hooley, C. "On Artin's conjecture." Journal für die reine und angewandte Mathematik 225 (1967): 209-220.

Imports (2)

def ArtinPrimitiveRootsConjecture.IsDedekindZeta Documented declaration: IsDedekindZeta line 62 source
Source documentation
Z is a Dedekind zeta function of the number field K: it is holomorphic away from $s = 1$ and agrees with the Dedekind zeta series of K on $\operatorname{Re} s > 1$, where that series converges. Such a Z is uniquely determined on $\mathbb{C} \setminus \{1\}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Complex
Proof uses: And, DifferentiableOn, Compl.compl, Set, Singleton.singleton, OfNat.ofNat, LT.lt, Real, Complex.re, Eq, NumberField.dedekindZeta
22 instances, coercions and auxiliary constants left out.
```
def IsDedekindZeta (K : Type*) [Field K] [NumberField K] (Z : ℂ → ℂ) : Prop :=
…
```
def ArtinPrimitiveRootsConjecture.DedekindZetaRH The Riemann hypothesis for the Dedekind zeta function line 68 source
Source documentation
The Riemann hypothesis for the Dedekind zeta function $\zeta_K$ of a number field $K$: every zero of (the analytic continuation of) $\zeta_K$ in the critical strip $0 < \operatorname{Re} s < 1$ has real part $\frac{1}{2}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField
Proof uses: Complex, ArtinPrimitiveRootsConjecture.IsDedekindZeta, LT.lt, Real, OfNat.ofNat, Complex.re, Eq, HDiv.hDiv
12 instances, coercions and auxiliary constants left out.
```
def DedekindZetaRH (K : Type*) [Field K] [NumberField K] : Prop :=
…
```
def ArtinPrimitiveRootsConjecture.HooleyHypothesis Documented declaration: HooleyHypothesis line 76 source
Source documentation
Hooley's hypothesis for $a$: the Riemann hypothesis holds for the Dedekind zeta function of the Kummer field $\mathbb{Q}(\zeta_k, a^{1/k})$, the splitting field of $X^k - a$ over $\mathbb{Q}$, for every squarefree $k$. This is the hypothesis under which Hooley [Ho67] proved Artin's conjecture.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int
Proof uses: Nat, Squarefree, ArtinPrimitiveRootsConjecture.DedekindZetaRH, Polynomial.SplittingField, Rat, HSub.hSub, Polynomial, HPow.hPow, Polynomial.X, RingHom, Polynomial.C
19 instances, coercions and auxiliary constants left out.
```
def HooleyHypothesis (a : ℤ) : Prop :=
…
```
abbrev ArtinPrimitiveRootsConjecture.S Let $S(a)$ be the set of primes such that $a$ is a primitive root modulo $p$ line 82 source
Source documentation
Let $S(a)$ be the set of primes such that $a$ is a primitive root modulo $p$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Set, Nat
Proof uses: Set.ofPred, And, Nat.Prime, Eq, orderOf, ZMod, HSub.hSub, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
```
abbrev S (a : ℤ) : Set ℕ :=
…
```
def ArtinPrimitiveRootsConjecture.ArtinConstant Artin's Constant is defined to be the product $$\prod_{p\ \text{prime}} \left(1 - \frac{1}{p(p - 1)}\right)$$ line 89 source
Source documentation
Artin's Constant is defined to be the product $$\prod_{p\ \text{prime}} \left(1 - \frac{1}{p(p - 1)}\right)$$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: tprod, Nat.Primes, HSub.hSub, OfNat.ofNat, HDiv.hDiv, HMul.hMul, Nat, Nat.Prime, SummationFilter.unconditional
16 instances, coercions and auxiliary constants left out.
```
noncomputable def ArtinConstant : ℝ :=
…
```
def ArtinPrimitiveRootsConjecture.powCorrectionFactor Documented declaration: powCorrectionFactor line 98 source
Source documentation
Artin's conjecture on $S(a)$ when $a = b^m$ is a power, where $m$ is odd and maximal, requires a correction factor to multiply ArtinConstant and is given by $$\prod_{p \mid m} \frac{p(p - 2)}{p^2 - p - 1}.$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Finset.prod, Nat.primeFactors, HDiv.hDiv, HMul.hMul, HSub.hSub, OfNat.ofNat, HPow.hPow
19 instances, coercions and auxiliary constants left out.
```
noncomputable def powCorrectionFactor (m : ℕ) : ℝ :=
…
```
def ArtinPrimitiveRootsConjecture.entanglementFactor Documented declaration: entanglementFactor line 110 source
Source documentation
Artin's conjecture on $S(a)$ when $a = b^m$ is a power, and the squarefree part of $b_0\equiv 1\pmod{4}$, requires a further correct factor to ArtinConstant * powCorrectionFactor m, which modifies primes which divide $\gcd(b_0, m)$ and primes which do not divide $m$ separately as $$ 1 - \prod_{p \mid \gcd(b_0, m)} \frac{1}{2 - p} \prod_{p \mid b_0, p\nmid m} \frac{1}{1 + p - p^2}.$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HSub.hSub, OfNat.ofNat, HMul.hMul, Finset.prod, Nat.primeFactors, Nat.gcd, Nat.squarefreePart, HDiv.hDiv, SDiff.sdiff, Finset, HAdd.hAdd, HPow.hPow
23 instances, coercions and auxiliary constants left out.
```
noncomputable def entanglementFactor (b : ℕ) (m : ℕ) : ℝ :=
…
```
theorem ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.i Artin's Conjecture on Primitive Roots, first half sorry line 120 source
Source documentation
Artin's Conjecture on Primitive Roots, first half. Let $a$ be an integer that is not a square number and not $−1$. Then the set $S(a)$ of primes $p$ such that $a$ is a primitive root modulo $p$ has a positive asymptotic density inside the set of primes. In particular, $S(a)$ is infinite.

depends on sorry what this means
Statement uses: Int, Not, IsSquare, Ne, Neg.neg, OfNat.ofNat, Exists, Real, And, GT.gt, Set.HasDensity, Nat, ArtinPrimitiveRootsConjecture.S, Set.ofPred, Nat.Prime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem artin_primitive_roots.parts.i (a : ℤ) (ha : ¬IsSquare a) (ha' : a ≠ -1) :
    ∃ x > 0, (S a).HasDensity x {p | p.Prime} := by
…
```
Mentions: ArtinPrimitiveRootsConjecture.S
theorem ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.parts.i Artin's Conjecture on Primitive Roots, first half, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields sorry line 130 source
Source documentation
Artin's Conjecture on Primitive Roots, first half, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields $\mathbb{Q}(\zeta_k, a^{1/k})$, $k$ squarefree [Ho67].

depends on sorry what this means
Statement uses: Int, Not, IsSquare, Ne, Neg.neg, OfNat.ofNat, ArtinPrimitiveRootsConjecture.HooleyHypothesis, Exists, Real, And, GT.gt, Set.HasDensity, Nat, ArtinPrimitiveRootsConjecture.S, Set.ofPred, Nat.Prime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem conditional_artin_primitive_roots.parts.i (a : ℤ) (ha : ¬IsSquare a) (ha' : a ≠ -1)
    (h : HooleyHypothesis a) :
    ∃ x > 0, (S a).HasDensity x {p | p.Prime} := by
…
```
Mentions: ArtinPrimitiveRootsConjecture.HooleyHypothesis, ArtinPrimitiveRootsConjecture.S
theorem ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.ii Artin's Conjecture on Primitive Roots, second half sorry line 143 source
Source documentation
Artin's Conjecture on Primitive Roots, second half. Write $a = a_0 b^2$ where $a_0$ is squarefree. Under the conditions that $a$ is not a perfect power and $a_0\not\equiv 1\pmod{4}$ (sequence A85397 in the OEIS), the density of the set $S(a)$ of primes $p$ such that $a$ is a primitive root modulo $p$ is independent of $a$ and equals Artin's constant.

depends on sorry what this means
Statement uses: Int, Eq, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, Ne, Squarefree, Not, Int.ModEq, Set.HasDensity, ArtinPrimitiveRootsConjecture.S, ArtinPrimitiveRootsConjecture.ArtinConstant, Set.ofPred, Nat.Prime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem artin_primitive_roots.parts.ii
    (a a_0 b : ℤ) (ha : a = a_0 * b ^ 2)
    (ha' : ∀ n m, m ≠ 1 → a ≠ n ^ m) (ha_0 : Squarefree a_0)
    (ha_0' : ¬a_0 ≡ 1 [ZMOD 4]) :
    (S a).HasDensity ArtinConstant {p | p.Prime} := by
…
```
Mentions: ArtinPrimitiveRootsConjecture.S, ArtinPrimitiveRootsConjecture.ArtinConstant
theorem ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.parts.ii Artin's Conjecture on Primitive Roots, second half, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields sorry line 157 source
Source documentation
Artin's Conjecture on Primitive Roots, second half, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields $\mathbb{Q}(\zeta_k, a^{1/k})$, $k$ squarefree [Ho67].

depends on sorry what this means
Statement uses: Int, Eq, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, Ne, Squarefree, Not, Int.ModEq, ArtinPrimitiveRootsConjecture.HooleyHypothesis, Set.HasDensity, ArtinPrimitiveRootsConjecture.S, ArtinPrimitiveRootsConjecture.ArtinConstant, Set.ofPred, Nat.Prime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem conditional_artin_primitive_roots.parts.ii
    (a a_0 b : ℤ) (ha : a = a_0 * b ^ 2)
    (ha' : ∀ n m, m ≠ 1 → a ≠ n ^ m) (ha_0 : Squarefree a_0)
    (ha_0' : ¬a_0 ≡ 1 [ZMOD 4])
    (h : HooleyHypothesis a) :
    (S a).HasDensity ArtinConstant {p | p.Prime} := by
…
```
Mentions: ArtinPrimitiveRootsConjecture.HooleyHypothesis, ArtinPrimitiveRootsConjecture.S, ArtinPrimitiveRootsConjecture.ArtinConstant
theorem ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_square_or_minus_one Documented declaration: part_ii_square_or_minus_one sorry line 172 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Int, Or, IsSquare, Eq, Neg.neg, OfNat.ofNat, Set.HasDensity, Nat, ArtinPrimitiveRootsConjecture.S, Real, Set.ofPred, Nat.Prime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem artin_primitive_roots.variants.part_ii_square_or_minus_one
    (a : ℤ) (ha : IsSquare a ∨ a = -1) :
    (S a).HasDensity 0 {p | p.Prime} := by
…
```
Mentions: ArtinPrimitiveRootsConjecture.S
theorem ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one Documented declaration: part_ii_power_squarefreePart_not_modeq_one sorry line 186 source
Source documentation
Artin's Conjecture on Primitive Roots, second half, power version If $a = b^m$ is a perfect odd power of a number $b$ whose squarefree part $b_0\not\equiv 1 \pmod{4}$, then the density of the set $S(a)$ of primes $p$ such that $a$ is a primitive root modulo $p$ is given by $$C\prod_{p \mid m} \frac{p(p - 2)}{p^2 - p - 1}$$, where $C$ is Artin's constant.

depends on sorry what this means
Statement uses: Nat, Eq, HPow.hPow, LT.lt, OfNat.ofNat, Ne, Odd, Not, Nat.ModEq, Nat.squarefreePart, Set.HasDensity, ArtinPrimitiveRootsConjecture.S, Int, HMul.hMul, Real, ArtinPrimitiveRootsConjecture.ArtinConstant, ArtinPrimitiveRootsConjecture.powCorrectionFactor, Set.ofPred, Nat.Prime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one
    (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v^u) (hm₁ : 1 < m)
    (hm₂ : Odd m) (hb' : ¬ b.squarefreePart ≡ 1 [MOD 4]) :
    (S a).HasDensity (ArtinConstant * powCorrectionFactor m) {p | p.Prime} := by
…
```
Mentions: ArtinPrimitiveRootsConjecture.S, ArtinPrimitiveRootsConjecture.ArtinConstant, ArtinPrimitiveRootsConjecture.powCorrectionFactor
theorem ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one Artin's Conjecture on Primitive Roots, second half, power version, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields sorry line 198 source
Source documentation
Artin's Conjecture on Primitive Roots, second half, power version, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields $\mathbb{Q}(\zeta_k, a^{1/k})$, $k$ squarefree [Ho67].

depends on sorry what this means
Statement uses: Nat, Eq, HPow.hPow, LT.lt, OfNat.ofNat, Ne, Odd, Not, Nat.ModEq, Nat.squarefreePart, ArtinPrimitiveRootsConjecture.HooleyHypothesis, Int, Set.HasDensity, ArtinPrimitiveRootsConjecture.S, HMul.hMul, Real, ArtinPrimitiveRootsConjecture.ArtinConstant, ArtinPrimitiveRootsConjecture.powCorrectionFactor, Set.ofPred, Nat.Prime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one
    (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v ^ u) (hm₁ : 1 < m)
    (hm₂ : Odd m) (hb' : ¬ b.squarefreePart ≡ 1 [MOD 4])
    (h : HooleyHypothesis a) :
    (S a).HasDensity (ArtinConstant * powCorrectionFactor m) {p | p.Prime} := by
…
```
Mentions: ArtinPrimitiveRootsConjecture.HooleyHypothesis, ArtinPrimitiveRootsConjecture.S, ArtinPrimitiveRootsConjecture.ArtinConstant, ArtinPrimitiveRootsConjecture.powCorrectionFactor
theorem ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one Documented declaration: part_ii_power_squarefreePart_modeq_one sorry line 216 source
Source documentation
Artin's Conjecture on Primitive Roots, second half, power version If $a = b^m$ is a perfect power of a number $b$ whose squarefree part $b_0\equiv 1 \pmod{4}$, then the density of the set $S(a)$ of primes $p$ such that $a$ is a primitive root modulo $p$ is given by $$C \left(\prod_{p \mid m} \frac{p(p-2)}{(p ^ 2 - p - 1)}\right) \left(1 - \prod_{p \mid \gcd(b_0, m)} \frac{1}{2 - p} \prod_{p \mid b_0, p\nmid m} \frac{1}{(1 + p - p ^ 2)}\right),$$ where $C$ is Artin's constant.

depends on sorry what this means
Statement uses: Nat, Eq, HPow.hPow, LT.lt, OfNat.ofNat, Ne, Odd, Nat.ModEq, Nat.squarefreePart, Set.HasDensity, ArtinPrimitiveRootsConjecture.S, Int, HMul.hMul, Real, ArtinPrimitiveRootsConjecture.ArtinConstant, ArtinPrimitiveRootsConjecture.powCorrectionFactor, ArtinPrimitiveRootsConjecture.entanglementFactor, Set.ofPred, Nat.Prime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one
    (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v ^ u) (hm₁ : 1 < m)
    (hm₂ : Odd m) (hb' : b.squarefreePart ≡ 1 [MOD 4]) :
    (S a).HasDensity
      (ArtinConstant * powCorrectionFactor m * entanglementFactor b m)
      {p | p.Prime} := by
…
```
Mentions: ArtinPrimitiveRootsConjecture.S, ArtinPrimitiveRootsConjecture.ArtinConstant, ArtinPrimitiveRootsConjecture.powCorrectionFactor, ArtinPrimitiveRootsConjecture.entanglementFactor
theorem ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one Artin's Conjecture on Primitive Roots, second half, power version, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields sorry line 230 source
Source documentation
Artin's Conjecture on Primitive Roots, second half, power version, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields $\mathbb{Q}(\zeta_k, a^{1/k})$, $k$ squarefree [Ho67].

depends on sorry what this means
Statement uses: Nat, Eq, HPow.hPow, LT.lt, OfNat.ofNat, Ne, Odd, Nat.ModEq, Nat.squarefreePart, ArtinPrimitiveRootsConjecture.HooleyHypothesis, Int, Set.HasDensity, ArtinPrimitiveRootsConjecture.S, HMul.hMul, Real, ArtinPrimitiveRootsConjecture.ArtinConstant, ArtinPrimitiveRootsConjecture.powCorrectionFactor, ArtinPrimitiveRootsConjecture.entanglementFactor, Set.ofPred, Nat.Prime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one
    (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v ^ u) (hm₁ : 1 < m)
    (hm₂ : Odd m) (hb' : b.squarefreePart ≡ 1 [MOD 4])
    (h : HooleyHypothesis a) :
    (S a).HasDensity
      (ArtinConstant * powCorrectionFactor m * entanglementFactor b m)
      {p | p.Prime} := by
…
```
Mentions: ArtinPrimitiveRootsConjecture.HooleyHypothesis, ArtinPrimitiveRootsConjecture.S, ArtinPrimitiveRootsConjecture.ArtinConstant, ArtinPrimitiveRootsConjecture.powCorrectionFactor, ArtinPrimitiveRootsConjecture.entanglementFactor