OAI/NumberTheory/CubicMoment/Theta/CubicThetaFrequencyTwist.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite arithmetic Fourier coefficient under a primary change of additive frequency. The relation is proved on the actual residue ring; it is independent of any continuation or theta coefficient formula.

  1. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_mul line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_cubeFrequency line 61