OAI/NumberTheory/Ostmann/QuadraticSieveMainCancellation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.QuadraticSieve.sq_sqrt_of_isSquare line 9
2. theorem OAI.Ostmann.QuadraticSieve.squareLift_mul_apply line 13
3. def OAI.Ostmann.QuadraticSieve.mainAlpha line 46
4. def OAI.Ostmann.QuadraticSieve.mainBeta line 49
5. theorem OAI.Ostmann.QuadraticSieve.mainAlpha_eq_function line 53
6. theorem OAI.Ostmann.QuadraticSieve.mainBeta_eq_function line 82
7. theorem OAI.Ostmann.QuadraticSieve.mainAlpha_eq_mainBeta line 119
8. theorem OAI.Ostmann.QuadraticSieve.mainAlpha_eq_mainBeta_of_squarefree line 123