OAI/NumberTheory/Ostmann/QuadraticSieveJacobiCharacter.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.QuadraticSieve.jacobiResidue line 7
  2. theorem OAI.Ostmann.QuadraticSieve.jacobiResidue_intCast line 9
  3. def OAI.Ostmann.QuadraticSieve.jacobiDirichletCharacterInt line 14
  4. theorem OAI.Ostmann.QuadraticSieve.jacobiDirichletCharacterInt_intCast line 32
  5. def OAI.Ostmann.QuadraticSieve.jacobiDirichletCharacter line 36
  6. theorem OAI.Ostmann.QuadraticSieve.jacobiDirichletCharacter_intCast line 39
  7. theorem OAI.Ostmann.QuadraticSieve.jacobiDirichletCharacter_natCast line 45
  8. theorem OAI.Ostmann.QuadraticSieve.jacobiDirichletCharacter_isQuadratic line 49
  9. theorem OAI.Ostmann.QuadraticSieve.jacobiDirichletCharacter_inv line 56
  10. theorem OAI.Ostmann.QuadraticSieve.jacobiDirichletCharacter_one_isPrimitive line 60
  11. theorem OAI.Ostmann.QuadraticSieve.jacobi_nat_modEq line 65
  12. theorem OAI.Ostmann.QuadraticSieve.exists_jacobi_neg_one_congr_one line 70
  13. theorem OAI.Ostmann.QuadraticSieve.prime_dvd_jacobiDirichletCharacter_conductor line 91
  14. theorem OAI.Ostmann.QuadraticSieve.jacobiDirichletCharacter_isPrimitive line 113