mathlib

4b4975cf - feat(<various>): add a bunch of lemmas for use with Jacobi symbols (#16290)

feat(<various>): add a bunch of lemmas for use with Jacobi symbols (#16290) This PR introduces a number of lemmas that will be needed for proving results about the Jacobi symbol (to be introduced in a follow-up PR). (Originally, the Jacobi symbol results were included here; see the discussion below.) Discussion on [Zuilp](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Jacobi.20symbol/near/295816984).