Commit 2024-06-10 04:35 d7681006
View on Github →refactor: move GaussSum directly under NumberTheory (#13540)
This moves NumberTheory.LegendreSymbol.GaussSum to NumberTheory.GaussSum.
Rationale: Gauss sums are useful beyond quadratic reciprocity (which was the original motivation to add them to Mathlib).
We use the opportunity to deal with some porting notes.