Commit 2022-08-09 19:12 4a1b5307
View on Github →feat(number_theory/legendre_symbol/quadratic_char): add results on special values (#15888) This uses the new results on Gauss sums to prove results on the values of quadratic characters at 2, -2 and odd primes. The next step will be to use these to prove Quadratic Reciprocity and the Second Supplementary Law for Legendre symbols. Here is the Zulip discussion on Gauss sums.