English
Let p and q be odd primes. Then the Legendre symbols satisfy (q/p) = (-1)^{((p-1)(q-1))/4} (p/q).
Русский
Пусть p и q — нечётные простые числа. Тогда квадратные символы удовлетворяют (q/p) = (-1)^{((p-1)(q-1))/4} (p/q).
LaTeX
$$$ \\left( \\frac{q}{p} \\right) = (-1)^{\\frac{(p-1)(q-1)}{4}} \\left( \\frac{p}{q} \\right) \\quad$ при $p,q$ простых нечётных.$$
Lean4
/-- The Law of Quadratic Reciprocity: if `p` and `q` are odd primes, then
`(q / p) = (-1)^((p-1)(q-1)/4) * (p / q)`. -/
theorem quadratic_reciprocity' (hp : p ≠ 2) (hq : q ≠ 2) :
legendreSym q p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p q :=
by
rcases eq_or_ne p q with h | h
· subst p
rw [(eq_zero_iff q q).mpr (mod_cast natCast_self q), mul_zero]
· have qr := congr_arg (· * legendreSym p q) (quadratic_reciprocity hp hq h)
have : ((q : ℤ) : ZMod p) ≠ 0 := mod_cast prime_ne_zero p q h
simpa only [mul_assoc, ← pow_two, sq_one p this, mul_one] using qr
