OAI/NumberTheory/CubicMoment/Angular/AngularStoppedSelectedRow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The selected-bin free-prime row with its actual full product, complementary exclusion and both stopping tests.

  1. def OAI.CubicFirstMoment.angular_stoppedSelectedPrimeRow line 16
  2. theorem OAI.CubicFirstMoment.angular_stopped_selected_prime_row_saving line 22