OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootMatrix.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The exact arithmetic subgroup for translations by 3x/p^3. It is needed to compare the cubic Hecke correlation with finite Fourier classes.

  1. abbrev OAI.CubicFirstMoment.cubicThetaPrimeCubeRootSubgroup line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootSubgroup_finiteIndex line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRoot_lower_division line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRoot_diagonal_division line 23
  5. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootMatrix line 29
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootMatrix_mem line 47
  7. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootConjugate line 68