OAI/NumberTheory/JointDickman/Arithmetic/HighBinPrimeWeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

High-bin avoidance is precisely a prime cutoff

  1. theorem OAI.JointDickman.highBinPrimeWeight line 10
  2. theorem OAI.JointDickman.largePrimeSet_cutoff_subset line 41
  3. theorem OAI.JointDickman.highBinPrimeDegree line 51