mathlib

8922aaa5 - feat(number_theory/legendre_symbol/norm_num): add file with `norm_num` extension for the Jacobi symbol (#16519)

feat(number_theory/legendre_symbol/norm_num): add file with `norm_num` extension for the Jacobi symbol (#16519) This PR adds the file `number_theory.legendre_symbol.norm_num`, which provides an extension to the `norm_num` tactic, so that it can compute the value of a Jacobi (or Legendre) symbol when the entries are concrete numbers. See this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Jacobi.20symbol/near/298768851) for discussion.