OAI/NumberTheory/Ostmann/QuadraticSieveSmoothingGcdSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.QuadraticSieve.quotientSupport_mul_mem line 7
2. theorem OAI.Ostmann.QuadraticSieve.quotientSupport_coprime line 12
3. theorem OAI.Ostmann.QuadraticSieve.quotientSupport_factor line 16
4. theorem OAI.Ostmann.QuadraticSieve.coefficientEnergy_quotientSupport_le line 22
5. theorem OAI.Ostmann.QuadraticSieve.quotientSupport_dyadic line 30
6. theorem OAI.Ostmann.QuadraticSieve.quotientSupport_one_lt line 41
7. theorem OAI.Ostmann.QuadraticSieve.gcdJacobiRow_zero_of_bad_factor line 51