OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootPowerOrthogonal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Vanishing of the second and fourth dilation pairings on the actual cubic root cover, forced by their nontrivial diagonal characters.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRoot_diagonal_character line 11
  2. def OAI.CubicFirstMoment.cubicThetaPrimeSixthPowerIwahori line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootPower_pair_invariant line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootPower_pair_zero_of_character line 43
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootSquare_pair_zero line 83
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFourth_pair_zero line 97