OAI/NumberTheory/JointDickman/Arithmetic/CandidateDefectPrimes.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite set of primes defective for candidate root comparison

  1. def OAI.JointDickman.auxiliaryDivisors line 11
  2. theorem OAI.JointDickman.auxiliaryDivisors_mass line 14
  3. def OAI.JointDickman.candidateDefectPrimes line 25
  4. theorem OAI.JointDickman.candidateDefectPrimes_mass line 32