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.