OAI/NumberTheory/CubicMoment/Theta/CubicThetaAdaptedCusp.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Choose the additive rational cusp lift with a lower-right entry zero modulo three, preserving the prescribed first column.

  1. def OAI.CubicFirstMoment.cubicThetaAdaptedCuspMatrix line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaAdaptedCuspMatrix_entries line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaAdaptedCuspMatrix_three line 25
  4. def OAI.CubicFirstMoment.cubicThetaAdaptedGaussMatrix line 32
  5. lemma OAI.CubicFirstMoment.cubicThetaAdaptedGaussMatrix_top line 36
  6. lemma OAI.CubicFirstMoment.cubicThetaAdaptedGaussMatrix_bottom line 41
  7. theorem OAI.CubicFirstMoment.cubicThetaAdaptedGaussMatrix_multiplier line 46