OAI/NumberTheory/CubicMoment/Decomposition/StoppedDistinguishedRow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Prime cancellation with the literal distinguished-coordinate bin, output interval and both stopping tests. The interval is derived, not assumed to describe the stopping support.

  1. def OAI.CubicFirstMoment.stoppedDistinguishedPrimeSet line 14
  2. theorem OAI.CubicFirstMoment.stopped_distinguished_prime_saving line 22