OAI/NumberTheory/DirichletL/Moments/AmplificationEligibility.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentAmplificationEligibility.exclusionIdeal line 15
2. def OAI.SevenEighths.CenteredMomentAmplificationEligibility.eligible line 17
3. theorem OAI.SevenEighths.CenteredMomentAmplificationEligibility.exclusionIdeal_ne_zero line 19
4. theorem OAI.SevenEighths.CenteredMomentAmplificationEligibility.exclusionIdeal_norm line 23
5. theorem OAI.SevenEighths.CenteredMomentAmplificationEligibility.eligible_not_dvd_row line 34
6. theorem OAI.SevenEighths.CenteredMomentAmplificationEligibility.eligible_coprime_divisor line 40
7. theorem OAI.SevenEighths.CenteredMomentAmplificationEligibility.uniform_eligible_pool line 46
8. theorem OAI.SevenEighths.CenteredMomentAmplificationEligibility.actual_eligible_amplification line 60