OAI/NumberTheory/Ostmann/QuadraticSieveDivisorDyadicBasic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticSieve.dyadicDivisors line 11
2. def OAI.Ostmann.QuadraticSieve.divisorDyadicDepth line 13
3. def OAI.Ostmann.QuadraticSieve.divisorDyadicIndices line 15
4. theorem OAI.Ostmann.QuadraticSieve.dyadicDivisors_card line 19
5. theorem OAI.Ostmann.QuadraticSieve.mem_dyadicDivisors_log line 23
6. theorem OAI.Ostmann.QuadraticSieve.dyadic_pair_mem line 27
7. theorem OAI.Ostmann.QuadraticSieve.divisorDyadicIndices_nonempty line 46
8. theorem OAI.Ostmann.QuadraticSieve.divisorDyadicIndices_card_le line 50
9. theorem OAI.Ostmann.QuadraticSieve.divisorDyadicIndices_scales line 54