OAI/NumberTheory/CubicMoment/Theta/CubicThetaSymbolKloostermanSymmetry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Hermitian inversion for the unramified local Kloosterman factor, including its common-factor zeros.

  1. lemma OAI.CubicFirstMoment.cubicThetaResidueSymbol_inverse line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaSymbolKloosterman_hermitian line 45
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeKloosterman_support_left line 72