OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimePowerFourier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The local conductor restriction for cubic Gauss coefficients at an unramified prime power. The weight is the literal cubic residue symbol.

  1. lemma OAI.CubicFirstMoment.cubicThetaSymbol_prime_pow line 11
  2. def OAI.CubicFirstMoment.cubicThetaLocalPrimePowerGauss line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerWeight_inflation line 23
  4. theorem OAI.CubicFirstMoment.cubicThetaLocalPrimePowerGauss_support line 36
  5. theorem OAI.CubicFirstMoment.cubicThetaLocalPrimePowerGauss_eq_zero line 48
  6. theorem OAI.CubicFirstMoment.cubicThetaLocalPrimePowerGauss_reduction line 54