OAI/NumberTheory/PrimePackets/PrimeSums.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.card_primeFactors_le_log line 35
  2. lemma OAI.PrimeDegreePackets.coprime_prime_sum_split line 57
  3. lemma OAI.PrimeDegreePackets.omitted_prime_tail line 87
  4. lemma OAI.PrimeDegreePackets.prime_sum_add_log_bad_le line 107
  5. theorem OAI.PrimeDegreePackets.coprime_prime_exponential_le_zeta line 127
  6. theorem OAI.PrimeDegreePackets.coprime_ideal_relative_interval_normalized line 183
  7. lemma OAI.PrimeDegreePackets.idealsOverPrime_prime line 230
  8. lemma OAI.PrimeDegreePackets.idealsOverPrime_norm_power line 234
  9. def OAI.PrimeDegreePackets.PrimaryIdeal line 243
  10. lemma OAI.PrimeDegreePackets.primary_ideal_norm_power line 246
  11. def OAI.PrimeDegreePackets.primaryIdealMultisetEquiv line 265
  12. def OAI.PrimeDegreePackets.primaryIdealNormEquiv line 303
  13. lemma OAI.PrimeDegreePackets.ennreal_tsum_multiset_prod line 332
  14. lemma OAI.PrimeDegreePackets.primaryIdealMultisetEquiv_val line 352
  15. lemma OAI.PrimeDegreePackets.primaryIdealNormEquiv_val line 355
  16. lemma OAI.PrimeDegreePackets.primary_ideal_inverse_norm_series line 359
  17. lemma OAI.PrimeDegreePackets.idealsOverPrime_norm_two_le line 389
  18. theorem OAI.PrimeDegreePackets.idealPrimeEuler_eq_primeIdeal_product line 401