mathlib

74a27133 - feat(number_theory/legendre_symbol/*): add some API for the Legendre and the Jacobi symbol (#19011)

feat(number_theory/legendre_symbol/*): add some API for the Legendre and the Jacobi symbol (#19011) This PR adds some additional API lemmas for the Legendre symbol (related to solutions mod `p` of `x^2-a*y^2 = 0`) and for the Jacobi symbol. These are useful for a project formalizing the proof that a certain diophantine equation has no integral solutions, but also appear to make sense more generally.