Legendre Symbol

Statement

For an odd prime $p$ and integer $a$, the Legendre symbol $\left(\frac{a}{p}\right)$ (also written $\text{legendreSym}\; p\; a$ in Lean) is defined as

Euler's criterion gives a computable formula: for $p \nmid a$,

In Mathlib this is legendreSym.eq_pow: the integer value of $\text{legendreSym}\; p\; a$ cast into $\mathbb{Z}/p\mathbb{Z}$ equals $(a \bmod p)^{p/2}$.

Visualization

Legendre symbol $\left(\frac{a}{7}\right)$ for $p = 7$, $a = 1,\ldots,6$:

$a$	$a^3 \bmod 7$	$\left(\frac{a}{7}\right)$
1	1	$+1$
2	1	$+1$ (2 is QR: $3^2=9\equiv 2$)
3	6 $\equiv -1$	$-1$ (3 is QNR)
4	1	$+1$ (4 $= 2^2$)
5	6 $\equiv -1$	$-1$ (5 is QNR)
6	6 $\equiv -1$	$-1$ (6 is QNR)

Check: QRs mod 7 are $\{1, 2, 4\}$ — three values, which is $(7-1)/2 = 3$. The product of all six symbols is $(-1)^3 = -1$.

Proof Sketch

1. The group $(\mathbb{Z}/p\mathbb{Z})^\times$ is cyclic of order $p-1$ by Primitive RootsPrimitive Roots$$g \text{ is a primitive root mod } p \iff \{g^0, g^1, \ldots, g^{p-2}\} = (\mathbb{Z}/p\mathbb{Z})^\times$$A primitive root mod p is a generator of the cyclic group (Z/pZ)*, existing for every prime pRead more →. Let $g$ be a generator; write $a = g^k$.
2. $a$ is a QR iff $k$ is even. The map $a \mapsto a^{(p-1)/2}$ sends $g^k$ to $g^{k(p-1)/2}$. Since $g^{p-1} = 1$, this is $1$ when $k$ is even and $-1$ when $k$ is odd.
3. This coincides with the Legendre symbol, establishing Euler's criterion.
4. Multiplicativity $\left(\frac{ab}{p}\right) = \left(\frac{a}{p}\right)\left(\frac{b}{p}\right)$ follows from the same power-map argument.

Connections

The Legendre symbol is the building block of 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 →, which relates $\left(\frac{p}{q}\right)$ and $\left(\frac{q}{p}\right)$ for distinct odd primes. The generalisation to composite moduli is the Jacobi SymbolJacobi Symbol$$\left(\frac{a}{n}\right) = \prod_{i} \left(\frac{a}{p_i}\right)^{e_i}$$The Jacobi symbol generalises the Legendre symbol to composite odd moduliRead more →.

/-- Euler's criterion in Mathlib: the cast of `legendreSym p a` into `ZMod p`
    equals `(a : ZMod p) ^ (p / 2)`. -/
theorem legendre_euler_criterion (p : ℕ) [Fact p.Prime] (a : ℤ) :
    (legendreSym p a : ZMod p) = (a : ZMod p) ^ (p / 2) :=
  legendreSym.eq_pow p a