OAI/NumberTheory/DirichletL/Hecke/PrimePowers.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.HeckePrimePowers.nonprime_primePow_powerful line 11
2. def OAI.SevenEighths.HeckePrimePowers.logWeight line 26
3. theorem OAI.SevenEighths.HeckePrimePowers.logWeight_nonneg line 28
4. theorem OAI.SevenEighths.HeckePrimePowers.logWeight_le_one line 31
5. theorem OAI.SevenEighths.HeckePrimePowers.logWeight_prime line 37
6. theorem OAI.SevenEighths.HeckePrimePowers.logWeight_eq_zero line 43
7. theorem OAI.SevenEighths.HeckePrimePowers.sum_prime_extraction line 46
8. theorem OAI.SevenEighths.HeckePrimePowers.prime_extraction_error line 61