https://people.epfl.ch/rodrigo.raya
This is an unofficial reimagining of the Archive of Formal Proofs
Gauss Sums and the Pólya–Vinogradov Inequalityby Rodrigo Raya and Manuel Eberl