OAI/NumberTheory/DirichletL/Hecke/Reciprocal.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.HeckeReciprocal.coefficients_sum_ne_zero_of_principal line 10
  2. theorem OAI.SevenEighths.HeckeReciprocal.dualScalar_ne_zero line 35
  3. theorem OAI.SevenEighths.HeckeReciprocal.principal_dual_constant_ne_zero line 42
  4. def OAI.SevenEighths.HeckeReciprocal.regularizedL line 48
  5. theorem OAI.SevenEighths.HeckeReciprocal.regularizedL_eq line 51
  6. theorem OAI.SevenEighths.HeckeReciprocal.regularizedL_at_one line 57
  7. theorem OAI.SevenEighths.HeckeReciprocal.regularizedL_ne_zero_at_one line 61
  8. theorem OAI.SevenEighths.HeckeReciprocal.regularizedL_differentiableAt line 67
  9. theorem OAI.SevenEighths.HeckeReciprocal.regularizedL_ne_zero line 71
  10. def OAI.SevenEighths.HeckeReciprocal.reciprocal line 84
  11. theorem OAI.SevenEighths.HeckeReciprocal.reciprocal_eq_inv line 87
  12. theorem OAI.SevenEighths.HeckeReciprocal.reciprocal_principal_one line 95
  13. theorem OAI.SevenEighths.HeckeReciprocal.reciprocal_differentiableAt line 98