Commit 2022-09-14 11:13 e1452ef2

chore(number_theory/legendre_symbol/): move zmod.{legendre|jacobi}_sym to other namespaces (#16461) This PR moves legendre_sym and jacobi_sym (and qr_sign) to the root namespace. It also moves definitions and lemmas named legendre_sym_... to the legendre_sym namespace and analogous for jacobi_sym_... and qr_sign_.... We change names like jacobi_sym_two to jacobi_sym.at_two. This mostly affects the files number_theory.legendre_symbol.quadratic_reciprocity and number_theory.legendre_symbol.jacobi_symbol. Note that names like exists_sq_eq_neg_one_iff have been left in zmod. We prefix quadratic_reciprocity* by legendre_sym to disambiguate with the versions for the Jacobi symbol. (The links in docs/100.yaml and docs/overview.yaml are updated accordingly.) We also move the results in number_theory.legendre_symbol.gauss_eisenstein_lemmas from the legendre_symbol namespace to the zmod namespace. See this Zulip thread and the comments at [#16395](https://github.com/leanprover-community/mathlib/pull/16395) for discussion.