OAI/NumberTheory/DirichletL/Moments/FixedQForcingCount.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFixedQForcingCount.goodSet line 20
2. def OAI.SevenEighths.CenteredMomentFixedQForcingCount.excludedSet line 23
3. def OAI.SevenEighths.CenteredMomentFixedQForcingCount.goodIdeal line 26
4. def OAI.SevenEighths.CenteredMomentFixedQForcingCount.excludedIdeal line 29
5. lemma OAI.SevenEighths.CenteredMomentFixedQForcingCount.prime_product_squarefree line 33
6. lemma OAI.SevenEighths.CenteredMomentFixedQForcingCount.prime_product_mem line 39
7. lemma OAI.SevenEighths.CenteredMomentFixedQForcingCount.goodIdeal_squarefree line 47
8. lemma OAI.SevenEighths.CenteredMomentFixedQForcingCount.goodIdeal_ne_zero line 53
9. lemma OAI.SevenEighths.CenteredMomentFixedQForcingCount.good_valuation_two line 57
10. lemma OAI.SevenEighths.CenteredMomentFixedQForcingCount.forcing_split line 64
11. lemma OAI.SevenEighths.CenteredMomentFixedQForcingCount.prime_dvd_of_not_coprime line 68
12. lemma OAI.SevenEighths.CenteredMomentFixedQForcingCount.excludedIdeal_dvd_radical line 75
13. lemma OAI.SevenEighths.CenteredMomentFixedQForcingCount.forcing_dvd_good_mul_radical line 89
14. lemma OAI.SevenEighths.CenteredMomentFixedQForcingCount.forcing_norm_le line 97
15. lemma OAI.SevenEighths.CenteredMomentFixedQForcingCount.fixed_radical_power_loss line 109
16. theorem OAI.SevenEighths.CenteredMomentFixedQForcingCount.actual_forcing_exceptional_count_fixedQ line 122
17. theorem OAI.SevenEighths.CenteredMomentFixedQForcingCount.actual_canonical_exceptional_count_fixedQ line 180