OAI/NumberTheory/Ostmann/QuadraticSieveExponentIteration.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.QuadraticSieve.ExponentBoundline 9 - theorem
OAI.Ostmann.QuadraticSieve.exponent_sum_absorbline 13 - theorem
OAI.Ostmann.QuadraticSieve.exponentBound_one_of_improvementline 31 - theorem
OAI.Ostmann.QuadraticSieve.epsilon_bound_of_exponent_improvementline 60