OAI/NumberTheory/CubicMoment/Theta/CubicThetaGaussConjugation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Complex conjugation of the finite arithmetic data used to normalize Patterson's theta series.

  1. theorem OAI.CubicFirstMoment.cubicTheta_gauss_conjugate line 11
  2. lemma OAI.CubicFirstMoment.cubicTheta_conjugate_lambda line 22
  3. lemma OAI.CubicFirstMoment.cubicTheta_squarefree_conjugate line 28