OAI/NumberTheory/CubicMoment/Theta/CubicThetaComplexPointMeasure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The already computed hyperbolic Jacobian also applies to the nonintegral prime normalizer on the same positive-height space.

  1. instance OAI.CubicFirstMoment.cubicThetaComplexPointAction_continuous line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaComplexPointMeasure_image line 22
  3. instance OAI.CubicFirstMoment.cubicThetaComplexPointMeasure_invariant line 38