Commit 2022-01-25 07:42 bf71feb0

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