OAI/NumberTheory/DirichletL/Detector/PrimePower.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbePrimePower.primeGauss line 13
2. def OAI.SevenEighths.ProbePrimePower.primePowerGauss line 17
3. theorem OAI.SevenEighths.ProbePrimePower.primePowerGauss_support line 21
4. theorem OAI.SevenEighths.ProbePrimePower.primePowerGauss_zero_off_support line 26
5. theorem OAI.SevenEighths.ProbePrimePower.primePowerGauss_lift line 32
6. theorem OAI.SevenEighths.ProbePrimePower.primePowerGauss_nonprincipal_extra_divisibility line 42
7. theorem OAI.SevenEighths.ProbePrimePower.primePowerGauss_principal line 58
8. theorem OAI.SevenEighths.ProbePrimePower.higher_outer_lift_annihilated line 75
9. def OAI.SevenEighths.ProbePrimePower.scalarKOne line 89
10. theorem OAI.SevenEighths.ProbePrimePower.scalarKOne_eq line 94