OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedNineGauss.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact evaluation of the finite ramified Gauss sum. The three ramified character exponents select three distinct additive congruence classes; this calculation is independent of residue identification.

  1. theorem OAI.CubicFirstMoment.cubicThetaRamifiedCharacter_power line 13
  2. def OAI.CubicFirstMoment.cubicThetaRamifiedNineGauss line 30
  3. theorem OAI.CubicFirstMoment.cubicThetaRamifiedNineGauss_eq line 35