mathlib

bf71feb0 - feat(number_theory/quadratic_reciprocity): generalise legendre_sym to allow integer first argument (#11573)

feat(number_theory/quadratic_reciprocity): generalise legendre_sym to allow integer first argument (#11573) Talking about the legendre symbol of -1 mod p is quite natural, so we generalize to include this case. So far in a minimal way without changing any existing lemmas