OAI/NumberTheory/CubicMoment/Theta/CubicThetaInversionGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The geometric inversion in the cubic theta transformation, restricted only by positive height and nonzero level. No automorphy law is assumed.

  1. def OAI.CubicFirstMoment.cubicThetaRadius line 10
  2. def OAI.CubicFirstMoment.cubicThetaInversion line 12
  3. lemma OAI.CubicFirstMoment.cubicThetaRadius_pos line 16
  4. lemma OAI.CubicFirstMoment.cubicThetaInversion_height_pos line 20
  5. lemma OAI.CubicFirstMoment.cubicThetaInversion_center line 24
  6. lemma OAI.CubicFirstMoment.cubicThetaInversion_radius line 35