OAI/NumberTheory/PrimePackets/IdealSupport.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.IdealSupportedAt line 25
  2. def OAI.PrimeDegreePackets.IdealCoprimeTo line 28
  3. lemma OAI.PrimeDegreePackets.idealSupportedAt_one line 31
  4. lemma OAI.PrimeDegreePackets.idealCoprimeTo_one line 37
  5. lemma OAI.PrimeDegreePackets.idealSupportedAt_mul line 42
  6. lemma OAI.PrimeDegreePackets.idealCoprimeTo_mul line 51
  7. lemma OAI.PrimeDegreePackets.idealSupportedAt_of_norm_eq_prime_pow line 58
  8. lemma OAI.PrimeDegreePackets.idealCoprimeTo_of_norm_eq_prime_pow line 66
  9. theorem OAI.PrimeDegreePackets.exists_ideal_support_split line 77
  10. lemma OAI.PrimeDegreePackets.ideal_support_norm_coprime line 102
  11. lemma OAI.PrimeDegreePackets.ideal_support_relprime line 107
  12. lemma OAI.PrimeDegreePackets.ideal_support_split_unique line 116
  13. def OAI.PrimeDegreePackets.coprimeIntegralIdeals line 138
  14. def OAI.PrimeDegreePackets.idealSupportMul line 141
  15. lemma OAI.PrimeDegreePackets.idealSupportMul_bijective line 146
  16. def OAI.PrimeDegreePackets.idealSupportEquiv line 156
  17. lemma OAI.PrimeDegreePackets.nonzeroIntegralIdealUnit_mul line 161
  18. lemma OAI.PrimeDegreePackets.completed_ideal_mul_off line 168
  19. lemma OAI.PrimeDegreePackets.globalIdealWeight_mul_coprime line 177
  20. theorem OAI.PrimeDegreePackets.weighted_ideal_convolution line 189
  21. def OAI.PrimeDegreePackets.completedOrderIdealModule line 217
  22. lemma OAI.PrimeDegreePackets.completedOrderIdealModule_le line 222
  23. lemma OAI.PrimeDegreePackets.completedOrderIdealModule_saturated line 228
  24. lemma OAI.PrimeDegreePackets.completedOrderIdealModule_pow_mem line 243
  25. theorem OAI.PrimeDegreePackets.patch_completedOrder_ideals line 255
  26. lemma OAI.PrimeDegreePackets.integralIdeal_norm_product_of_off line 289
  27. lemma OAI.PrimeDegreePackets.integralIdeal_support_of_off line 318
  28. lemma OAI.PrimeDegreePackets.modelIdeal_pow_mem line 332
  29. lemma OAI.PrimeDegreePackets.ideal_pi_injective line 349
  30. lemma OAI.PrimeDegreePackets.dvr_power_injective line 362
  31. theorem OAI.PrimeDegreePackets.primaryIdealValuations_surjective line 370
  32. def OAI.PrimeDegreePackets.primaryIdealValuationEquiv line 409
  33. lemma OAI.PrimeDegreePackets.integralIdeal_norm_eq_shell_product line 415
  34. lemma OAI.PrimeDegreePackets.ennreal_inv_prod_finite line 429
  35. lemma OAI.PrimeDegreePackets.inverse_shellNorm_sum line 433
  36. theorem OAI.PrimeDegreePackets.primaryIntegralIdeals_inverse_norm_series line 448