OAI/NumberTheory/DirichletL/Hecke/Dyadic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.HeckeDyadic.NonzeroIdeal line 11
2. instance OAI.SevenEighths.HeckeDyadic.(instance at line 13) line 13
3. instance OAI.SevenEighths.HeckeDyadic.(instance at line 14) line 14
4. def OAI.SevenEighths.HeckeDyadic.norm line 16
5. theorem OAI.SevenEighths.HeckeDyadic.norm_pos line 18
6. def OAI.SevenEighths.HeckeDyadic.coefficient line 22
7. theorem OAI.SevenEighths.HeckeDyadic.coefficient_norm_le line 25
8. theorem OAI.SevenEighths.HeckeDyadic.coefficient_zero line 34
9. def OAI.SevenEighths.HeckeDyadic.shift line 40
10. theorem OAI.SevenEighths.HeckeDyadic.shift_re line 42
11. def OAI.SevenEighths.HeckeDyadic.summand line 44
12. def OAI.SevenEighths.HeckeDyadic.polynomial line 48
13. theorem OAI.SevenEighths.HeckeDyadic.summand_finite_support line 51
14. def OAI.SevenEighths.HeckeDyadic.series line 69
15. theorem OAI.SevenEighths.HeckeDyadic.series_eq_tsum line 72