OAI/NumberTheory/DirichletL/Hecke/FiniteDeletion.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.HeckeFiniteDeletion.factors line 12
  2. theorem OAI.SevenEighths.HeckeFiniteDeletion.factors_eq line 16
  3. theorem OAI.SevenEighths.HeckeFiniteDeletion.factors_differentiable line 25
  4. theorem OAI.SevenEighths.HeckeFiniteDeletion.factors_ne_zero line 32
  5. theorem OAI.SevenEighths.HeckeFiniteDeletion.LFunction_eq_of_mask_right line 41
  6. theorem OAI.SevenEighths.HeckeFiniteDeletion.regularizedL_analytic line 50
  7. theorem OAI.SevenEighths.HeckeFiniteDeletion.regularizedL_eq_of_mask line 56
  8. theorem OAI.SevenEighths.HeckeFiniteDeletion.LFunction_eq_of_mask line 76
  9. theorem OAI.SevenEighths.HeckeFiniteDeletion.regularizedL_one_ne_zero_iff line 86
  10. theorem OAI.SevenEighths.HeckeFiniteDeletion.principal_iff_of_mask line 97
  11. theorem OAI.SevenEighths.HeckeFiniteDeletion.LFunction_eq_of_mask_nonprincipal line 105
  12. theorem OAI.SevenEighths.HeckeFiniteDeletion.LFunction_eq_of_mask_nonpole line 126
  13. theorem OAI.SevenEighths.HeckeFiniteDeletion.exists_primitive_same_zeros line 135
  14. theorem OAI.SevenEighths.HeckeFiniteDeletion.exists_primitive_zero line 147