OAI/NumberTheory/DirichletL/Hecke/BoundaryIntegration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.HeckeFamily.LFunction_one_ne_zero_quadratic line 10
2. theorem OAI.SevenEighths.HeckeFamily.LFunction_boundary_ne_zero line 18
3. theorem OAI.SevenEighths.HeckeFamily.LFunction_one_ne_zero_nonprincipal line 51
4. theorem OAI.SevenEighths.HeckeFamily.LFunction_ne_zero_of_re_eq_one line 58
5. theorem OAI.SevenEighths.HeckeFamily.LFunction_ne_zero_of_one_le_re line 69