OAI/NumberTheory/JointDickman/Amplification/ExceptionalProductIntegral.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Auxiliary prime products on the actual exceptional frequency set
- theorem
OAI.JointDickman.exceptional_product_integralline 11