OAI/NumberTheory/JointDickman/Amplification/RamareIntegralBound.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The prime/cofactor integral with auxiliary large values discharged
- theorem
OAI.JointDickman.ramare_product_integral_boundline 11