OAI/NumberTheory/DirichletL/CubicSieve/Sharp.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.CubicSieve.hasCubicExponent_four_thirdsline 8 - lemma
OAI.SevenEighths.CubicSieve.four_thirds_le_crossline 45 - theorem
OAI.SevenEighths.CubicSieve.sieveNorm_sharpline 55