mathlib3

6f3426cf - chore(number_theory/legendre_symbol/quadratic_char): golf some proofs (#13926)