OAI/NumberTheory/CubicMoment/Decomposition/StoppedCommonSquareDivisor.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual common-factor rows still satisfy the bounded-coefficient estimate after a small square-divisor rescales the outer variable.

  1. theorem OAI.CubicFirstMoment.rough_square_divisor_common_blocks line 13