mathlib

d795ea4b - feat(number_theory/legendre_symbol/quadratic_reciprocity): Alternate forms of `exists_sq_eq_neg_one` (#13594)

feat(number_theory/legendre_symbol/quadratic_reciprocity): Alternate forms of `exists_sq_eq_neg_one` (#13594) Also, renamed `exists_sq_eq_neg_one_iff_mod_four_ne_three` to `exists_sq_eq_neg_one` for consistency with `exists_sq_eq_two` and for convenience.