OAI/NumberTheory/Ostmann/QuadraticSieveGcdSeparation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.QuadraticSieve.sum_moebius_divisors_complex line 9
  2. theorem OAI.Ostmann.QuadraticSieve.common_divisors_eq_filter_Icc line 16
  3. theorem OAI.Ostmann.QuadraticSieve.sum_common_moebius line 26
  4. theorem OAI.Ostmann.QuadraticSieve.coprime_bilinear_moebius line 32
  5. theorem OAI.Ostmann.QuadraticSieve.coprime_jacobi_bilinear_moebius line 69
  6. theorem OAI.Ostmann.QuadraticSieve.shared_divisor_restriction line 96
  7. theorem OAI.Ostmann.QuadraticSieve.norm_moebius_complex_le_one line 99
  8. theorem OAI.Ostmann.QuadraticSieve.coprime_bilinear_norm_le line 102
  9. theorem OAI.Ostmann.QuadraticSieve.coprime_bilinear_norm_sq_le line 118
  10. theorem OAI.Ostmann.QuadraticSieve.sum_coprime_bilinear_norm_sq_le line 130
  11. theorem OAI.Ostmann.QuadraticSieve.sum_divisor_restricted_norm_sq line 143
  12. theorem OAI.Ostmann.QuadraticSieve.sum_divisor_restricted_norm_sq_le line 155