OAI/NumberTheory/CubicMoment/Theta/CubicThetaKubotaInteger.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Invariance under the whole integer modular group, derived from its proved S,T generation and the two explicit reciprocity calculations.

  1. lemma OAI.CubicFirstMoment.cubicThetaKubotaConjugate_one line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaKubotaConjugate_mul line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaKubotaConjugate_inverse line 23
  4. def OAI.CubicFirstMoment.cubicThetaKubotaPreservers line 27
  5. def OAI.CubicFirstMoment.cubicThetaIntegerEmbedding line 40
  6. lemma OAI.CubicFirstMoment.cubicThetaIntegerEmbedding_S line 43
  7. lemma OAI.CubicFirstMoment.cubicThetaIntegerEmbedding_T line 51
  8. theorem OAI.CubicFirstMoment.cubicThetaKubotaValue_conjugate_integer line 59
  9. theorem OAI.CubicFirstMoment.cubicThetaKubotaValue_integer line 82