OAI/NumberTheory/JointDickman/Amplification/OutsideCandidateProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Product comparison over the unoccupied primes

  1. def OAI.JointDickman.outsideCandidateProductMass line 10
  2. theorem OAI.JointDickman.outsideCandidateProduct_l1 line 17