OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeDoubleRootMatrix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeDouble_primary line 12
  2. abbrev OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootSubgroup line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootSubgroup_finiteIndex line 17
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRoot_lower_division line 21
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRoot_diagonal_division line 26
  6. def OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootMatrix line 32
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootMatrix_mem line 50
  8. def OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootConjugate line 71