Commit 2022-09-08 20:32 d2d66526

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