OAI/NumberTheory/CubicMoment/Theta/CubicThetaKubotaReal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The multiplier is trivial on the real part of the principal group, as required for its eventual extension across SL(2,Z).

  1. lemma OAI.CubicFirstMoment.cubicThetaKubotaValue_conjugate_fixed line 10
  2. theorem OAI.CubicFirstMoment.cubicThetaKubotaValue_real line 19