OAI/NumberTheory/Ostmann/Quadratic/QuadraticGaussSign.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The positive branch of the actual squarefree Jacobi Gauss sum

The prime case uses AINTLIB's quadratic Gauss-sum evaluation. The passage to odd squarefree moduli uses the exact Chinese remainder formula.

  1. theorem OAI.Ostmann.quadraticGaussMultiplier_prime line 17
  2. theorem OAI.Ostmann.quadraticGaussMultiplier_one line 28
  3. theorem OAI.Ostmann.quadraticGaussMultiplier_odd_squarefree line 35