OAI/NumberTheory/PrimePackets/LocalEuler.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.primaryIdealSingletonEquiv line 39
  2. theorem OAI.PrimeDegreePackets.actual_localZ_eq_idealPrimeEuler line 56
  3. theorem OAI.PrimeDegreePackets.actualLocalZ_eq_badPrimeEuler line 81
  4. lemma OAI.PrimeDegreePackets.IdealCoprimeTo_primeFactors_iff line 98
  5. def OAI.PrimeDegreePackets.nonzeroIdealNormFiberEquiv line 111
  6. lemma OAI.PrimeDegreePackets.integralIdeal_norm_tsum line 120
  7. def OAI.PrimeDegreePackets.coprimeIdealSubtypeEquiv line 146
  8. lemma OAI.PrimeDegreePackets.coprimeIntegralIdeal_norm_tsum line 154
  9. lemma OAI.PrimeDegreePackets.coprimeIdeal_interval_tsum line 188
  10. def OAI.PrimeDegreePackets.weightedIdealInterval line 204
  11. theorem OAI.PrimeDegreePackets.weightedIdealInterval_convolution line 212
  12. theorem OAI.PrimeDegreePackets.primaryIdeal_reciprocal_tail line 230
  13. lemma OAI.PrimeDegreePackets.coprimeIdeal_interval_elementary line 269
  14. theorem OAI.PrimeDegreePackets.weightedIdeal_large_norm_bound line 302
  15. lemma OAI.PrimeDegreePackets.dedekindZeta_real_eq_terms line 356
  16. lemma OAI.PrimeDegreePackets.dedekindZeta_real_nonneg line 362
  17. lemma OAI.PrimeDegreePackets.dedekindZeta_real_antitone line 367
  18. lemma OAI.PrimeDegreePackets.dedekindZeta_log_scale_le line 383
  19. theorem OAI.PrimeDegreePackets.coprime_ideal_scaled_interval line 414