OAI/NumberTheory/CubicMoment/Theta/CubicThetaKubotaConjugation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Invariance of the cubic multiplier under the two integral modular generators, as needed to extend it to the group of DR v3 Section 5.1.

  1. lemma OAI.CubicFirstMoment.cubicSymbol_primary_lower_add line 11
  2. def OAI.CubicFirstMoment.cubicThetaKubotaConjugate line 19
  3. def OAI.CubicFirstMoment.cubicThetaModularS line 28
  4. def OAI.CubicFirstMoment.cubicThetaModularT line 31
  5. lemma OAI.CubicFirstMoment.cubicThetaKubotaConjugate_S_entries line 34
  6. lemma OAI.CubicFirstMoment.cubicThetaKubotaConjugate_T_entries line 43
  7. theorem OAI.CubicFirstMoment.cubicThetaKubotaValue_conjugate_S line 52
  8. theorem OAI.CubicFirstMoment.cubicThetaKubotaValue_conjugate_T line 60