OAI/NumberTheory/DirichletL/Hecke/Dirichlet.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.HeckeDirichlet.modulus line 12
  2. theorem OAI.SevenEighths.HeckeDirichlet.modulus_ne_bot line 14
  3. theorem OAI.SevenEighths.HeckeDirichlet.quotient_modulus_zero line 18
  4. theorem OAI.SevenEighths.HeckeDirichlet.norm_span_dvd line 22
  5. theorem OAI.SevenEighths.HeckeDirichlet.quotient_unit_of_norm_unit line 31
  6. def OAI.SevenEighths.HeckeDirichlet.residue line 45
  7. theorem OAI.SevenEighths.HeckeDirichlet.residue_mk line 61
  8. theorem OAI.SevenEighths.HeckeDirichlet.residue_unit_trivial line 64
  9. def OAI.SevenEighths.HeckeDirichlet.character line 71
  10. theorem OAI.SevenEighths.HeckeDirichlet.elementCoeff_character line 74
  11. theorem OAI.SevenEighths.HeckeDirichlet.idealCoeff_character line 77
  12. theorem OAI.SevenEighths.HeckeDirichlet.moebius_idealCoeff_character line 83
  13. theorem OAI.SevenEighths.HeckeDirichlet.inverseSeries_eq_pairInverse_LSeries line 94
  14. theorem OAI.SevenEighths.HeckeDirichlet.LFunction_eq_dirichlet_product_right line 112
  15. theorem OAI.SevenEighths.HeckeDirichlet.LFunction_eq_dirichlet_product line 128
  16. theorem OAI.SevenEighths.HeckeDirichlet.dirichlet_seven_eighths_of_hecke line 158
  17. theorem OAI.SevenEighths.HeckeDirichlet.zeta_seven_eighths_of_hecke line 171