OAI/NumberTheory/CubicMoment/Estimates/PrimeIdealPrimaryTransfer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact passage from complete prime ideals to the manuscript's unique primary prime representatives when the ramified coefficient vanishes.

  1. lemma OAI.CubicFirstMoment.prime_idealExponent_single line 14
  2. lemma OAI.CubicFirstMoment.prime_idealPrimaryGenerator line 25
  3. lemma OAI.CubicFirstMoment.primeCutoff_image_idealExponent line 32
  4. theorem OAI.CubicFirstMoment.idealPrimeChebyshev_primary_sum line 50