OAI/NumberTheory/Ostmann/QuadraticSieveMainCancellationBasic.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.QuadraticSieve.isSquare_mul_iff_of_coprime line 9
  2. def OAI.Ostmann.QuadraticSieve.squareLift line 20
  3. theorem OAI.Ostmann.QuadraticSieve.squareLift_apply_sq line 23
  4. theorem OAI.Ostmann.QuadraticSieve.squareLift_apply_of_not_square line 27
  5. theorem OAI.Ostmann.QuadraticSieve.squareLift_isMultiplicative line 30
  6. def OAI.Ostmann.QuadraticSieve.divisorMoebius line 52
  7. theorem OAI.Ostmann.QuadraticSieve.divisorMoebius_apply line 55
  8. theorem OAI.Ostmann.QuadraticSieve.divisorMoebius_isMultiplicative line 58
  9. def OAI.Ostmann.QuadraticSieve.squarefreeIndicator line 67
  10. theorem OAI.Ostmann.QuadraticSieve.squarefreeIndicator_apply line 70
  11. theorem OAI.Ostmann.QuadraticSieve.squarefreeIndicator_isMultiplicative line 75
  12. def OAI.Ostmann.QuadraticSieve.coprimeSquarefreeIndicator line 78
  13. theorem OAI.Ostmann.QuadraticSieve.coprimeSquarefreeIndicator_apply line 81
  14. theorem OAI.Ostmann.QuadraticSieve.coprimeSquarefreeIndicator_isMultiplicative line 91