OAI/NumberTheory/DirichletL/CubicSieve/Gcd.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CubicSieve.cubicRow line 13
2. lemma OAI.SevenEighths.CubicSieve.cubicRow_mul line 16
3. lemma OAI.SevenEighths.CubicSieve.cubicRow_square_eq_star line 20
4. lemma OAI.SevenEighths.CubicSieve.cubicRow_common_mask line 24
5. lemma OAI.SevenEighths.CubicSieve.cubicRow_common_mobius line 32
6. lemma OAI.SevenEighths.CubicSieve.cubic_admissible_of_dvd line 39
7. lemma OAI.SevenEighths.CubicSieve.cubic_admissible_quotient line 47
8. lemma OAI.SevenEighths.CubicSieve.cubicRow_divisor_factor line 51
9. def OAI.SevenEighths.CubicSieve.cubicGcdTerm line 56
10. theorem OAI.SevenEighths.CubicSieve.cubicGcdTerm_eq_quotient line 61
11. theorem OAI.SevenEighths.CubicSieve.cubic_weighted_energy_eq_gcd_blocks line 90