# Documentation

## 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 #

### 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 ()] (hp : p 2) :

legendreSym p 2 is given by χ₈ p.

theorem legendreSym.at_neg_two {p : } [Fact ()] (hp : p 2) :

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

theorem ZMod.exists_sq_eq_two_iff {p : } [Fact ()] (hp : p 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 ()] (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 ()] [Fact ()] (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 ()] [Fact ()] (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 ()] [Fact ()] (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 ()] [Fact ()] (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 ()] [Fact ()] (hp1 : p % 4 = 1) (hq1 : q 2) :

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 ()] [Fact ()] (hp3 : p % 4 = 3) (hq3 : q % 4 = 3) (hpq : p q) :

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.