Quadratic Reciprocity

Statement

For distinct odd primes $p$ and $q$:

where $\left(\frac{a}{p}\right)$ is the Legendre symbol — equal to $1$ if $a$ is a quadratic residue mod $p$, and $-1$ otherwise.

In words: $p$ is a square mod $q$ and $q$ is a square mod $p$, unless both $p \equiv q \equiv 3 \pmod{4}$, in which case exactly one is a square mod the other.

Supplements

The first supplement states:

The second supplement states:

Historical Note

Gauss called this the "golden theorem" (theorema aureum) and published six different proofs during his lifetime. Over 240 proofs are now known, using techniques from combinatorics, algebra, analysis, and algebraic geometry.

Connections

The proof relies on Fermat's Little TheoremFermat's Little Theorem$$a^p \equiv a \pmod{p}$$For prime p, a^p is congruent to a mod pRead more →. Some modern proofs use ideas from Galois theoryFundamental Theorem of Galois Theory$$\{\text{intermediate fields}\} \longleftrightarrow \{\text{subgroups of } \text{Gal}(K/F)\}$$Bijection between intermediate fields and subgroups of the Galois groupRead more →.

/-- Quadratic reciprocity for distinct odd primes. The Legendre symbol
    `legendreSym p q` is Mathlib's `(a/p)` defined via Euler's
    criterion. For odd `p`, the integer division `p / 2` equals
    `(p-1) / 2`, so the exponent matches the textbook form
    `((p-1)/2) · ((q-1)/2)`. -/
theorem quadratic_reciprocity {p q : ℕ} [Fact p.Prime] [Fact q.Prime]
    (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) :
    legendreSym q p * legendreSym p q = (-1) ^ (p / 2 * (q / 2)) :=
  legendreSym.quadratic_reciprocity hp hq hpq