OAI/NumberTheory/CubicMoment/Estimates/SmallPartSizes.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Subpower local data satisfy the quantitative conductor margins.

  1. theorem OAI.CubicFirstMoment.eventual_small_part_conductor_size line 11
  2. theorem OAI.CubicFirstMoment.eventual_small_part_modulus_size line 42
  3. lemma OAI.CubicFirstMoment.small_part_smaller_than_row line 61