OAI/NumberTheory/DirichletL/CubicSieve/Mobius.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CubicSieve.elementQuotient line 12
2. lemma OAI.SevenEighths.CubicSieve.elementQuotient_mul line 14
3. lemma OAI.SevenEighths.CubicSieve.elementQuotient_injective line 18
4. def OAI.SevenEighths.CubicSieve.dividedRows line 22
5. lemma OAI.SevenEighths.CubicSieve.sum_divisible_rows line 25
6. lemma OAI.SevenEighths.CubicSieve.dividedRows_ne_zero line 38
7. lemma OAI.SevenEighths.CubicSieve.dividedRows_norm_le line 46
8. lemma OAI.SevenEighths.CubicSieve.cubicRow_mul_argument line 62
9. lemma OAI.SevenEighths.CubicSieve.totalQuotient_cubic_admissible line 66
10. def OAI.SevenEighths.CubicSieve.descendedCoefficient line 74
11. def OAI.SevenEighths.CubicSieve.residualGram line 78
12. lemma OAI.SevenEighths.CubicSieve.residualGram_rescale line 84
13. lemma OAI.SevenEighths.CubicSieve.ideal_dvd_span_iff_generator line 100
14. lemma OAI.SevenEighths.CubicSieve.sum_dividedRows_residualGram_rescale line 107
15. theorem OAI.SevenEighths.CubicSieve.cubic_gcd_mobius_descent line 118