OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeReductionResidue.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The translation selected by the actual row completion is the inverse of 9n modulo its prime power. Thus its choice agrees with finite Fourier reindexing and with the original period-three lattice.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeReductionTranslation line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReductionTranslation_three line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReductionTranslation_congruence line 22
  4. def OAI.CubicFirstMoment.cubicThetaPrimeCubeReductionTranslationUnit line 30
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeReductionTranslation_residue line 39