OAI/NumberTheory/CubicMoment/Angular/AngularStoppedSelectedBeta.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Selected-side prime cancellation applies to the literal stoppedBeta coefficient, with its global-largest role selected exactly.

  1. theorem OAI.CubicFirstMoment.angular_stoppedBeta_selected_identity line 14