OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootDeepCharacter.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A nontrivial diagonal character deep enough to normalize the actual cubic root cover, for the intermediate-valuation cancellation.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeSixthIwahori line 13
  2. def OAI.CubicFirstMoment.cubicThetaPrimeSixthCubeIwahori line 17
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeSixthCharacter_nontrivial line 21
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootIwahoriImage_fundamental line 51