OAI/NumberTheory/CubicMoment/Decomposition/StoppedCommonRemainder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

All nonunit common factors of an active rough coefficient are restored. The three explicit costs are the rough small factors, the power-saving large factors, and their exact zero mode.

  1. theorem OAI.CubicFirstMoment.bounded_rough_common_remainder line 14