OAI/NumberTheory/DirichletL/Hecke/StripActual.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.SevenEighths.HeckeStripActual.(instance at line 15) line 15
2. def OAI.SevenEighths.HeckeStripActual.conductor line 20
3. theorem OAI.SevenEighths.HeckeStripActual.conductor_ge_one line 22
4. theorem OAI.SevenEighths.HeckeStripActual.completionScale_eq_inv line 28
5. theorem OAI.SevenEighths.HeckeStripActual.completionScale_cpow line 38
6. theorem OAI.SevenEighths.HeckeStripActual.completedL_eq_standard line 47
7. theorem OAI.SevenEighths.HeckeStripActual.LFunction_norm_le line 56
8. theorem OAI.SevenEighths.HeckeStripActual.pair_strong line 70
9. theorem OAI.SevenEighths.HeckeStripActual.LFunction_eq_uncompleted line 81
10. theorem OAI.SevenEighths.HeckeStripActual.functional_equation_left line 112
11. theorem OAI.SevenEighths.HeckeStripActual.LFunction_exp_growth line 151
12. theorem OAI.SevenEighths.HeckeStripActual.uniform_strip_bound line 172