OAI/NumberTheory/CubicMoment/Theta/CubicThetaExtendedGroup.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's group Gamma_2 generated by Gamma_1(3) and SL(2,Z). Normality of the principal group gives a concrete two-factor description.

  1. def OAI.CubicFirstMoment.cubicThetaExtendedGroup line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaExtendedGroup_eq_sup line 24
  3. def OAI.CubicFirstMoment.cubicThetaExtendedPrincipal line 39
  4. def OAI.CubicFirstMoment.cubicThetaExtendedInteger line 42
  5. lemma OAI.CubicFirstMoment.cubicThetaExtended_decomposition line 45
  6. def OAI.CubicFirstMoment.cubicThetaPrincipalInclusion line 50
  7. def OAI.CubicFirstMoment.cubicThetaIntegerInclusion line 55