OAI/NumberTheory/PrimePackets/SplitEuler.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.mem_idealsOverPrime_iff line 11
  2. def OAI.PrimeDegreePackets.primeIdealTowerEquiv line 24
  3. lemma OAI.PrimeDegreePackets.primeIdealTowerEquiv_val line 50
  4. def OAI.PrimeDegreePackets.primeIdealEulerFactor line 56
  5. lemma OAI.PrimeDegreePackets.primeIdealEulerFactor_eq_pow line 59
  6. lemma OAI.PrimeDegreePackets.dedekindZeta_hasProd line 74
  7. lemma OAI.PrimeDegreePackets.primeEuler_denominator_ne_zero_at_one line 102
  8. lemma OAI.PrimeDegreePackets.primeIdealEulerFactor_ne_zero_at_one line 113
  9. lemma OAI.PrimeDegreePackets.primeIdealEulerFactor_continuousAt_one line 119
  10. lemma OAI.PrimeDegreePackets.primeIdealEulerFactor_ne_zero line 127
  11. lemma OAI.PrimeDegreePackets.dedekindZeta_ratio_eq_finite_product line 140
  12. lemma OAI.PrimeDegreePackets.dedekindZeta_ratio_tendsto_zero line 155
  13. theorem OAI.PrimeDegreePackets.degree_eq_one_of_localEulerFactor_eq_pow line 187