OAI/NumberTheory/Ostmann/QuadraticSieveGaussBridgeCRT.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticSieve.crtLeftAddChar line 7
2. def OAI.Ostmann.QuadraticSieve.crtRightAddChar line 17
3. lemma OAI.Ostmann.QuadraticSieve.crtAddChar_apply line 27
4. lemma OAI.Ostmann.QuadraticSieve.crtLeftAddChar_isPrimitive line 37
5. lemma OAI.Ostmann.QuadraticSieve.crtRightAddChar_isPrimitive line 47
6. theorem OAI.Ostmann.QuadraticSieve.jacobiDirichletCharacter_crt line 57
7. theorem OAI.Ostmann.QuadraticSieve.quadratic_sum_crt line 69
8. theorem OAI.Ostmann.QuadraticSieve.jacobi_gauss_crt line 93