OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeHeckeRelation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Eliminate the two actual prime-free twists to obtain the unramified three-frequency relation in the initial half-plane.

  1. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_primeShift line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeFactors_product line 31
  3. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_primeHecke line 50