OAI/NumberTheory/DirichletL/CubicSieve/PairPrimes.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CubicSieve.pairPrime line 11
2. instance OAI.SevenEighths.CubicSieve.pairPrime_maximal line 14
3. lemma OAI.SevenEighths.CubicSieve.pairPrime_good line 18
4. lemma OAI.SevenEighths.CubicSieve.pairPrime_coprime line 24
5. lemma OAI.SevenEighths.CubicSieve.pairPrime_product line 43
6. def OAI.SevenEighths.CubicSieve.pairExponent line 48
7. lemma OAI.SevenEighths.CubicSieve.pairExponent_nonprincipal line 51
8. lemma OAI.SevenEighths.CubicSieve.primeIndex_cubic_row line 58
9. lemma OAI.SevenEighths.CubicSieve.primeIndex_conjugate_cubic_row line 64
10. lemma OAI.SevenEighths.CubicSieve.pairPrime_row line 76
11. lemma OAI.SevenEighths.CubicSieve.pairPrime_modulus line 85