OAI/NumberTheory/DirichletL/IdealEuler.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.IdealEuler.normWeight line 15
  2. def OAI.SevenEighths.IdealEuler.weighted line 28
  3. def OAI.SevenEighths.IdealEuler.series line 34
  4. def OAI.SevenEighths.IdealEuler.inverseSeries line 36
  5. theorem OAI.SevenEighths.IdealEuler.weighted_summable_norm line 39
  6. theorem OAI.SevenEighths.IdealEuler.weighted_summable line 48
  7. theorem OAI.SevenEighths.IdealEuler.inverse_summable_norm line 52
  8. theorem OAI.SevenEighths.IdealEuler.series_eq_LSeries line 60
  9. theorem OAI.SevenEighths.IdealEuler.inverseSeries_mul_series line 65
  10. theorem OAI.SevenEighths.IdealEuler.series_ne_zero line 106
  11. theorem OAI.SevenEighths.IdealEuler.inverseSeries_eq_inv line 113
  12. theorem OAI.SevenEighths.IdealEuler.primeValueHom_eq line 120
  13. theorem OAI.SevenEighths.IdealEuler.prime_summable_norm line 129
  14. theorem OAI.SevenEighths.IdealEuler.prime_norm_lt_one line 133
  15. theorem OAI.SevenEighths.IdealEuler.local_factor_ne_zero line 144
  16. theorem OAI.SevenEighths.IdealEuler.inverseSeries_euler line 148
  17. theorem OAI.SevenEighths.IdealEuler.euler_hasProd line 155
  18. theorem OAI.SevenEighths.IdealEuler.series_euler line 169
  19. def OAI.SevenEighths.IdealEuler.deletePrimes line 174
  20. theorem OAI.SevenEighths.IdealEuler.deletePrimes_prime line 178
  21. theorem OAI.SevenEighths.IdealEuler.deletePrimes_norm_le_one line 191
  22. theorem OAI.SevenEighths.IdealEuler.deletePrimes_apply line 199
  23. theorem OAI.SevenEighths.IdealEuler.deletePrimes_primeSet_apply line 225
  24. theorem OAI.SevenEighths.IdealEuler.series_deletePrimes line 248
  25. theorem OAI.SevenEighths.IdealEuler.series_of_coprime_mask line 277
  26. theorem OAI.SevenEighths.IdealEuler.series_ofResidue_source_mask line 289
  27. theorem OAI.SevenEighths.IdealEuler.exists_primitive_series_associate line 302