OAI/NumberTheory/CubicMoment/Angular/AngularStoppedSelectedDistinguished.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The selected-divisor role with the actual distinguished-tuple coefficient. Its roughness and coefficient bound are proved internally.

  1. theorem OAI.CubicFirstMoment.angular_stoppedBeta_selected_distinguished_saving line 19