OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeDilation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The unramified arithmetic correspondence acts on the actual hyperbolic Eisenstein family, with its cubic diagonal twist retained.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeSquareRoot line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeSquareRoot_ne_zero line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeSquareRoot_sq line 19
  4. def OAI.CubicFirstMoment.cubicThetaPrimeDilation line 25
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeDilation_intertwines line 29
  6. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_prime_dilation_twist line 63