OAI/NumberTheory/Ostmann/QuadraticSieveSignedSupport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.QuadraticSieve.signedSquarefreeUpTo line 7
  2. theorem OAI.Ostmann.QuadraticSieve.mem_signedSquarefreeUpTo line 11
  3. theorem OAI.Ostmann.QuadraticSieve.mem_signedSquarefreeUpTo_iff_natAbs line 18
  4. theorem OAI.Ostmann.QuadraticSieve.squarefree_odd_factor line 34
  5. def OAI.Ostmann.QuadraticSieve.signedSquarefreeMultipliers line 48
  6. theorem OAI.Ostmann.QuadraticSieve.mem_signedSquarefreeMultipliers line 50
  7. theorem OAI.Ostmann.QuadraticSieve.card_signedSquarefreeMultipliers line 54
  8. theorem OAI.Ostmann.QuadraticSieve.signedSquarefreeMultiplier_ne_zero line 57
  9. theorem OAI.Ostmann.QuadraticSieve.signedSquarefreeMultiplier_injective line 61
  10. theorem OAI.Ostmann.QuadraticSieve.exists_signedSquarefree_factor line 67
  11. theorem OAI.Ostmann.QuadraticSieve.signedSquarefreeUpTo_subset_biUnion line 84