OAI/NumberTheory/DirichletL/Hecke/Euler.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.SevenEighths.HeckeFamily.(instance at line 9) line 9
2. theorem OAI.SevenEighths.HeckeFamily.idealCoeff_norm_le_one line 11
3. theorem OAI.SevenEighths.HeckeFamily.idealTerm_eq_weighted line 15
4. theorem OAI.SevenEighths.HeckeFamily.LFunction_eq_series line 25
5. theorem OAI.SevenEighths.HeckeFamily.LFunction_ne_zero_of_one_lt_re line 30
6. theorem OAI.SevenEighths.HeckeFamily.inverseSeries_mul_LFunction line 35
7. theorem OAI.SevenEighths.HeckeFamily.LFunction_eq_normFiber_LSeries line 40