OAI/NumberTheory/CubicMoment/Estimates/SmallPartGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Conductor size and coprimality after the actual small-prime split.

  1. lemma OAI.CubicFirstMoment.primaryOutsidePart_dvd line 9
  2. lemma OAI.CubicFirstMoment.outside_parts_coprime line 13
  3. lemma OAI.CubicFirstMoment.outside_parts_coprime_local line 19
  4. lemma OAI.CubicFirstMoment.smallPartModulus_ne_zero line 30
  5. lemma OAI.CubicFirstMoment.smallPartModulus_norm_le line 37
  6. lemma OAI.CubicFirstMoment.primaryOutsidePart_nonunit line 49