OAI/NumberTheory/CubicMoment/Decomposition/StoppedEmptyTuple.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

With no distinguished prime coordinates, the largest prime can only occur in the selected divisor. This removes an artificial nonempty-tuple restriction from the stopped-coefficient sequence estimate.

  1. theorem OAI.CubicFirstMoment.stopped_distinguished_empty line 14