OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeGauss.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Normalization of the first local cubic Fourier factor. The inverse different in the additive pairing contributes exactly the cubic character of lambda; the remaining Gauss sum is the original normalized one.

  1. lemma OAI.CubicFirstMoment.cubicThetaResidueFourier_lambda line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeFourier_one_one line 26