OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootTraceNormalized.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact normalized trace pairing. No Hecke eigenvalue or local coefficient relation is postulated in constructing this identity.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootTrace_scalar line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootTrace_normalized_smooth line 36
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootTrace_normalized line 56