OAI/NumberTheory/CubicMoment/Estimates/SmallPartCharacter.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Literal finite-character factorization at the small conductor primes.

  1. lemma OAI.CubicFirstMoment.mixedCubic_modulus_mul line 13
  2. lemma OAI.CubicFirstMoment.small_outside_mixedCubic line 20
  3. def OAI.CubicFirstMoment.smallPartResidueTwist line 30
  4. lemma OAI.CubicFirstMoment.smallPartResidueTwist_units line 36
  5. lemma OAI.CubicFirstMoment.smallPartResidueTwist_primary line 44
  6. lemma OAI.CubicFirstMoment.primarySmallTwistSmoothSum_small_parts line 55
  7. lemma OAI.CubicFirstMoment.primaryOutsidePart_injOn_small_fiber line 68
  8. lemma OAI.CubicFirstMoment.primaryOutsidePart_norm_le line 77
  9. lemma OAI.CubicFirstMoment.primaryOutsidePart_norm_lower line 82