Quadratic reciprocity.

Main results

We prove the law of quadratic reciprocity, see legendreSym.quadratic_reciprocity and legendreSym.quadratic_reciprocity', as well as the interpretations in terms of existence of square roots depending on the congruence mod 4, ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one and ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three.

We also prove the supplementary laws that give conditions for when 2 or -2 is a square modulo a prime p: legendreSym.at_two and ZMod.exists_sq_eq_two_iff for 2 and legendreSym.at_neg_two and ZMod.exists_sq_eq_neg_two_iff for -2.

Implementation notes

The proofs use results for quadratic characters on arbitrary finite fields from NumberTheory.LegendreSymbol.QuadraticChar.GaussSum, which in turn are based on properties of quadratic Gauss sums as provided by NumberTheory.LegendreSymbol.GaussSum.

Tags

quadratic residue, quadratic nonresidue, Legendre symbol, quadratic reciprocity

The value of the Legendre symbol at 2 and -2

See jacobiSym.at_two and jacobiSym.at_neg_two for the corresponding statements for the Jacobi symbol.

theorem legendreSym.at_two {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) : legendreSym p 2 = ZMod.χ₈ ↑p

legendreSym p 2 is given by χ₈ p.

theorem legendreSym.at_neg_two {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) : legendreSym p (-2) = ZMod.χ₈' ↑p

legendreSym p (-2) is given by χ₈' p.

theorem ZMod.exists_sq_eq_two_iff {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) : IsSquare 2 ↔ p % 8 = 1 ∨ p % 8 = 7

2 is a square modulo an odd prime p iff p is congruent to 1 or 7 mod 8.

theorem ZMod.exists_sq_eq_neg_two_iff {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) : IsSquare (-2) ↔ p % 8 = 1 ∨ p % 8 = 3

-2 is a square modulo an odd prime p iff p is congruent to 1 or 3 mod 8.

The Law of Quadratic Reciprocity

See jacobiSym.quadratic_reciprocity and variants for a version of Quadratic Reciprocity for the Jacobi symbol.

theorem legendreSym.quadratic_reciprocity {p : ℕ} {q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) : legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

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 legendreSym.quadratic_reciprocity' {p : ℕ} {q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) : legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q

The Law of Quadratic Reciprocity: if p and q are odd primes, then (q / p) = (-1)^((p-1)(q-1)/4) * (p / q).

theorem legendreSym.quadratic_reciprocity_one_mod_four {p : ℕ} {q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p % 4 = 1) (hq : q ≠ 2) : legendreSym q ↑p = legendreSym p ↑q

The Law of Quadratic Reciprocity: if p and q are odd primes and p % 4 = 1, then (q / p) = (p / q).

theorem legendreSym.quadratic_reciprocity_three_mod_four {p : ℕ} {q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p % 4 = 3) (hq : q % 4 = 3) : legendreSym q ↑p = -legendreSym p ↑q

The Law of Quadratic Reciprocity: if p and q are primes that are both congruent to 3 mod 4, then (q / p) = -(p / q).

theorem ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one {p : ℕ} {q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp1 : p % 4 = 1) (hq1 : q ≠ 2) : IsSquare ↑q ↔ IsSquare ↑p

If p and q are odd primes and p % 4 = 1, then q is a square mod p iff p is a square mod q.

theorem ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three {p : ℕ} {q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp3 : p % 4 = 3) (hq3 : q % 4 = 3) (hpq : p ≠ q) : IsSquare ↑q ↔ ¬IsSquare ↑p

If p and q are distinct primes that are both congruent to 3 mod 4, then q is a square mod p iff p is a nonsquare mod q.