Jacobi Symbol

Statement

Let $n = p_1^{e_1} \cdots p_k^{e_k}$ be an odd positive integer. The Jacobi symbol is defined by

where each factor is a Legendre symbol. In Mathlib this is jacobiSym a n with notation J(a | n).

Key properties:

• $J(a \mid 1) = 1$ for all $a$ (jacobiSym.one_right).
• Multiplicativity in both arguments.
• Quadratic reciprocity: for odd coprime $m, n$,

Warning: $J(a \mid n) = 1$ does not imply $a$ is a QR mod $n$ when $n$ is composite.

Visualization

Worked computation of $J(2 \mid 15)$ via Jacobi reciprocity:

Factorisation: $15 = 3 \times 5$.

Step 1 — split by definition:

Step 2 — evaluate each Legendre symbol using Euler's criterion:

Step 3 — multiply:

Yet 2 is not a QR mod 15 (no $x$ with $x^2 \equiv 2 \pmod{15}$), illustrating the warning above.

Proof Sketch

1. The Jacobi symbol is defined as a product of Legendre symbols over the prime factorisation.
2. jacobiSym.one_right: when $n = 1$ the product is empty, so the symbol is $1$.
3. Quadratic reciprocity for Jacobi symbols is deduced from the Legendre version by induction on the prime factorisations, tracking the sign $(-1)^{\frac{m-1}{2}\cdot\frac{n-1}{2}}$.
4. Multiplicativity follows from multiplicativity of Legendre symbols.

Connections

The Jacobi symbol is a computational tool for Quadratic ReciprocityQuadratic Reciprocity$$\left(\frac{p}{q}\right)\left(\frac{q}{p}\right) = (-1)^{\frac{p-1}{2}\cdot\frac{q-1}{2}}$$Relationship between solvability of quadratic congruences for two odd primesRead more → — testing reciprocity for composite moduli uses it directly. The Legendre SymbolLegendre Symbol$$\left(\frac{a}{p}\right) = a^{(p-1)/2} \bmod p$$The Legendre symbol (a|p) encodes whether a is a quadratic residue mod a prime pRead more → is the prime-modulus special case.

open scoped NumberTheorySymbols in
/-- The Jacobi symbol J(a | 1) equals 1 for all integers a.
    Direct alias of `jacobiSym.one_right`. -/
theorem jacobi_one_right (a : ℤ) : J(a | 1) = 1 :=
  jacobiSym.one_right a