OAI/NumberTheory/CubicMoment/Angular/AngularStoppedDistinguishedRow.lean

GitHub source file

1 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. theorem OAI.CubicFirstMoment.angular_stopped_distinguished_prime_saving line 17