English
If p and q are distinct odd primes, then (q/p)(p/q) = (−1)^{(p−1)(q−1)/4}.
Русский
Если p и q — различные нечётные простые, то (q/p)(p/q) = (−1)^{(p−1)(q−1)/4}.
LaTeX
$$$\left(\frac{q}{p}\right)\left(\frac{p}{q}\right)=(-1)^{\frac{(p-1)(q-1)}{4}}$$$
Lean4
/-- **The Law of Quadratic Reciprocity**: if `p` and `q` are distinct odd primes, then
`(q / p) * (p / q) = (-1)^((p-1)(q-1)/4)`. -/
theorem quadratic_reciprocity (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) :
legendreSym q p * legendreSym p q = (-1) ^ (p / 2 * (q / 2)) :=
by
have hp₁ := (Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left hp
have hq₁ := (Prime.eq_two_or_odd <| @Fact.out q.Prime _).resolve_left hq
have hq₂ : ringChar (ZMod q) ≠ 2 := (ringChar_zmod_n q).substr hq
have h := quadraticChar_odd_prime ((ringChar_zmod_n p).substr hp) hq ((ringChar_zmod_n p).substr hpq)
rw [card p] at h
have nc : ∀ n r : ℕ, ((n : ℤ) : ZMod r) = n := fun n r => by norm_cast
have nc' : (((-1) ^ (p / 2) : ℤ) : ZMod q) = (-1) ^ (p / 2) := by norm_cast
rw [legendreSym, legendreSym, nc, nc, h, map_mul, mul_rotate', mul_comm (p / 2), ← pow_two,
quadraticChar_sq_one (prime_ne_zero q p hpq.symm), mul_one, pow_mul, χ₄_eq_neg_one_pow hp₁, nc', map_pow,
quadraticChar_neg_one hq₂, card q, χ₄_eq_neg_one_pow hq₁]
