OAI/NumberTheory/CubicMoment/Theta/CubicThetaPointMeasurePositive.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual hyperbolic measure is positive on every nonempty open subset of the positive-height space.

  1. instance OAI.CubicFirstMoment.cubicThetaPointMeasure_openPositive line 13