OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteConductor.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Additive conductors of the actual finite Fourier pairing. A function that factors through a smaller residue ring has Fourier support in the annihilator of the reduction kernel.

  1. lemma OAI.CubicFirstMoment.finiteFourier_translation_support line 12
  2. theorem OAI.CubicFirstMoment.residueFourier_reduction_support line 40
  3. theorem OAI.CubicFirstMoment.residueFourier_inflation_support line 53