OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeFourierNormalization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The branch Gauss multiplier in the original arithmetic additive normalization. The factor at three cancels the inverse different.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstFourier_additive line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstFourier_quotient line 22