mathlib3

d2d66526 - feat(number_theory/legendre_symbol/jacobi_symbol): add new file with the definition and properties of the Jacobi symbol (#16395)

feat(number_theory/legendre_symbol/jacobi_symbol): add new file with the definition and properties of the Jacobi symbol (#16395) This PR consists of a new file, `number_theory.legendre_symbol.jacobi_symbol`, that contains a definition of the Jacobi symbol (and sets up notation `[a | b]ⱼ` for it) and then proves a number of results, e.g., multiplicativity in both arguments, expressions for the cases `a = -1`, `a = 2`, `a = -2`, and several versions of quadratic reciprocity. It also proves that the symbol depends on a only through its residue class `mod b` and that it depends on `b` only through its residue class `mod 4*a` (quadratic reciprocity is needed for the latter). The code has already been quite thoroughly reviewed while it was part of #16290 (which then was reduced to the auxiliary results needed for the Jacobi symbol code). Discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Jacobi.20symbol/near/295816984)