mathlib3

4a1b5307 - feat(number_theory/legendre_symbol/quadratic_char): add results on special values (#15888)

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](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Gauss.20sums/near/292231902) is the Zulip discussion on Gauss sums.