OAI/NumberTheory/CubicMoment/Angular/AngularScaleFirstNoStopTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal ordinary-height no-stop row in the prime tail has the published Type-I saving. Its failed first-stage prefix is preserved.

  1. theorem OAI.CubicFirstMoment.angular_scaleFirstTailNoStopRow_finite_bound line 15