OAI/NumberTheory/CubicMoment/Decomposition/StoppedCommonPowers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Large common factors use the proved power bound only after their exact zero mode is removed. No roughness or cancellation of quotient rows is assumed.

  1. lemma OAI.CubicFirstMoment.rough_common_small_quotient line 14
  2. lemma OAI.CubicFirstMoment.rough_common_large_outer line 20
  3. theorem OAI.CubicFirstMoment.bounded_large_common_nonzero line 36