OAI/NumberTheory/CubicMoment/Theta/CubicThetaNineCusp.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A prescribed first column with lower-right entry divisible by nine. This makes the common-lattice additive phase a literal residue character.

  1. lemma OAI.CubicFirstMoment.cubicTheta_coprime_nine line 11
  2. def OAI.CubicFirstMoment.cubicThetaInverseNine line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaInverseNine_spec line 18
  4. def OAI.CubicFirstMoment.cubicThetaNineGaussMatrix line 25
  5. lemma OAI.CubicFirstMoment.cubicThetaNineGaussMatrix_entries line 30
  6. lemma OAI.CubicFirstMoment.cubicThetaNineGaussMatrix_nine line 48
  7. lemma OAI.CubicFirstMoment.cubicThetaNineGaussMatrix_primary line 54
  8. theorem OAI.CubicFirstMoment.cubicThetaNineGaussMatrix_multiplier line 60