OAI/NumberTheory/PrimePackets/IdealCoefficients.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.Sieve.powerfulMoment_one_le line 33
  2. theorem OAI.PrimeDegreePackets.Sieve.corrected_relative_interval line 38
  3. theorem OAI.PrimeDegreePackets.Sieve.divisor_bounded_relative_interval line 88
  4. def OAI.PrimeDegreePackets.idealCoefficient line 125
  5. lemma OAI.PrimeDegreePackets.idealCoefficient_pos line 129
  6. lemma OAI.PrimeDegreePackets.idealCoefficient_one line 133
  7. lemma OAI.PrimeDegreePackets.ideal_eq_of_dvd_of_norm_eq line 136
  8. lemma OAI.PrimeDegreePackets.ideals_relprime_of_norm_coprime line 145
  9. lemma OAI.PrimeDegreePackets.ideal_multiplication_injective line 153
  10. lemma OAI.PrimeDegreePackets.prime_pow_dvd_coprime_product line 175
  11. lemma OAI.PrimeDegreePackets.ideal_split_norm line 182
  12. def OAI.PrimeDegreePackets.idealNormProductEquiv line 228
  13. lemma OAI.PrimeDegreePackets.idealCoefficient_multiplicative line 242
  14. lemma OAI.PrimeDegreePackets.ideal_factor_prime_power line 254
  15. lemma OAI.PrimeDegreePackets.ideal_factor_count_le line 269
  16. def OAI.PrimeDegreePackets.idealsOverPrime line 285
  17. lemma OAI.PrimeDegreePackets.ideal_factor_mem_over line 288
  18. lemma OAI.PrimeDegreePackets.idealsOverPrime_card_le line 299
  19. lemma OAI.PrimeDegreePackets.idealCoefficient_prime_le line 305
  20. def OAI.PrimeDegreePackets.padMultiset line 329
  21. lemma OAI.PrimeDegreePackets.decode_padMultiset line 334
  22. lemma OAI.PrimeDegreePackets.card_le_of_multiset_encoding line 348
  23. lemma OAI.PrimeDegreePackets.idealCoefficient_prime_pow_le line 365
  24. theorem OAI.PrimeDegreePackets.idealCoefficient_le_divisor line 392
  25. def OAI.PrimeDegreePackets.idealCoefficientReal line 407
  26. lemma OAI.PrimeDegreePackets.idealCoefficientReal_multiplicative line 411
  27. lemma OAI.PrimeDegreePackets.idealCoefficientReal_nonneg line 417
  28. lemma OAI.PrimeDegreePackets.idealCoefficient_summatory_limit line 420
  29. lemma OAI.PrimeDegreePackets.idealCoefficient_LSeriesSummable line 441
  30. def OAI.PrimeDegreePackets.realDirichletTerm line 448
  31. lemma OAI.PrimeDegreePackets.realDirichletTerm_ofReal line 452
  32. lemma OAI.PrimeDegreePackets.idealCoefficient_real_summable line 460
  33. lemma OAI.PrimeDegreePackets.idealCoefficient_LSeries_eq line 466
  34. lemma OAI.PrimeDegreePackets.idealDirichlet_eq_dedekindZeta line 474