Commit 2023-05-15 06:03 74a27133

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.