OAI/NumberTheory/DirichletL/CubicSieve/Gauss.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CubicSieve.cubicQuotientCharacter line 11
2. lemma OAI.SevenEighths.CubicSieve.cubicQuotientCharacter_mk line 24
3. lemma OAI.SevenEighths.CubicSieve.cubicQuotientCharacter_cube line 28
4. lemma OAI.SevenEighths.CubicSieve.cubicQuotientCharacter_neg_one line 41
5. def OAI.SevenEighths.CubicSieve.quotientCharacterTransport line 51
6. def OAI.SevenEighths.CubicSieve.principalCubicCharacter line 58
7. lemma OAI.SevenEighths.CubicSieve.principalCubicCharacter_mk line 63
8. lemma OAI.SevenEighths.CubicSieve.principalCubicCharacter_neg_one line 68
9. lemma OAI.SevenEighths.CubicSieve.gaussTwo_eq_gaussSum line 73
10. lemma OAI.SevenEighths.CubicSieve.gaussSum_inverse_of_even line 82
11. lemma OAI.SevenEighths.CubicSieve.cubic_pair_cross_phase line 91
12. def OAI.SevenEighths.CubicSieve.cubicPairGauss line 102
13. theorem OAI.SevenEighths.CubicSieve.cubicPairGauss_separation line 113