OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootOrbitOrthogonal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Distinct fractional translates of the original global space are orthogonal, and all are orthogonal to its Weyl translate.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_translate_pair_zero line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootLift_translate_pair_zero line 26
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootOrbit_pair_zero line 49