OAI/NumberTheory/DirichletL/CubicSieve/QuotientColumns.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CubicSieve.finite_sum_restrict line 12
2. lemma OAI.SevenEighths.CubicSieve.cubicSmoothedCoprime_restrict line 21
3. def OAI.SevenEighths.CubicSieve.quotientColumn line 36
4. def OAI.SevenEighths.CubicSieve.quotientCoefficient line 39
5. lemma OAI.SevenEighths.CubicSieve.quotientColumn_injective line 43
6. lemma OAI.SevenEighths.CubicSieve.quotientColumn_admissible line 48
7. lemma OAI.SevenEighths.CubicSieve.cubic_quotient_in_shell line 52
8. lemma OAI.SevenEighths.CubicSieve.compact_descendant_restrict line 71
9. lemma OAI.SevenEighths.CubicSieve.quotientCoefficient_energy line 89