# mathlibdocumentation

The main results are the law of quadratic reciprocity, quadratic_reciprocity, as well as the interpretations in terms of existence of square roots depending on the congruence mod 4, exists_sq_eq_prime_iff_of_mod_four_eq_one, and exists_sq_eq_prime_iff_of_mod_four_eq_three.

Also proven are conditions for -1 and 2 to be a square modulo a prime, exists_sq_eq_neg_one_iff_mod_four_ne_three and exists_sq_eq_two_iff

## Implementation notes #

The proof of quadratic reciprocity implemented uses Gauss' lemma and Eisenstein's lemma

theorem zmod.euler_criterion_units (p : ) [fact (nat.prime p)] (x : units (zmod p)) :
(∃ (y : units (zmod p)), y ^ 2 = x) x ^ (p / 2) = 1

Euler's Criterion: A unit x of zmod p is a square if and only if x ^ (p / 2) = 1.

theorem zmod.euler_criterion (p : ) [fact (nat.prime p)] {a : zmod p} (ha : a 0) :
(∃ (y : zmod p), y ^ 2 = a) a ^ (p / 2) = 1

Euler's Criterion: a nonzero a : zmod p is a square if and only if x ^ (p / 2) = 1.

theorem zmod.exists_sq_eq_neg_one_iff_mod_four_ne_three (p : ) [fact (nat.prime p)] :
(∃ (y : zmod p), y ^ 2 = -1) p % 4 3
theorem zmod.pow_div_two_eq_neg_one_or_one (p : ) [fact (nat.prime p)] {a : zmod p} (ha : a 0) :
a ^ (p / 2) = 1 a ^ (p / 2) = -1
@[simp]
theorem zmod.wilsons_lemma (p : ) [fact (nat.prime p)] :
(p - 1)! = -1

Wilson's Lemma: the product of 1, ..., p-1 is -1 modulo p.

@[simp]
theorem zmod.prod_Ico_one_prime (p : ) [fact (nat.prime p)] :
∏ (x : ) in p, x = -1
theorem Ico_map_val_min_abs_nat_abs_eq_Ico_map_id (p : ) [hp : fact (nat.prime p)] (a : zmod p) (hap : a 0) :
multiset.map (λ (x : ), (a * x).val_min_abs.nat_abs) (p / 2).succ).val = multiset.map (λ (a : ), a) (p / 2).succ).val

The image of the map sending a non zero natural number x ≤ p / 2 to the absolute value of the element of interger in the interval (-p/2, p/2] congruent to a * x mod p is the set of non zero natural numbers x such that x ≤ p / 2

theorem div_eq_filter_card {a b c : } (hb0 : 0 < b) (hc : a / b c) :
a / b = (finset.filter (λ (x : ), x * b a) c.succ)).card
def zmod.legendre_sym (a p : ) :

The Legendre symbol of a and p is an integer defined as

• 0 if a is 0 modulo p;
• 1 if a ^ (p / 2) is 1 modulo p (by euler_criterion this is equivalent to “a is a square modulo p”);
• -1 otherwise.
Equations
theorem zmod.legendre_sym_eq_pow (a p : ) [hp : fact (nat.prime p)] :
p) = a ^ (p / 2)
theorem zmod.legendre_sym_eq_one_or_neg_one (a p : ) (ha : a 0) :
= -1 = 1
theorem zmod.legendre_sym_eq_zero_iff (a p : ) :
= 0 a = 0
theorem zmod.gauss_lemma (p : ) [fact (nat.prime p)] {a : } [fact (p % 2 = 1)] (ha0 : a 0) :
= (-1) ^ (finset.filter (λ (x : ), p / 2 < ((a) * x).val) (p / 2).succ)).card

Gauss' lemma. The legendre symbol can be computed by considering the number of naturals less than p/2 such that (a * x) % p > p / 2

theorem zmod.legendre_sym_eq_one_iff (p : ) [fact (nat.prime p)] {a : } (ha0 : a 0) :
= 1 ∃ (b : zmod p), b ^ 2 = a
theorem zmod.eisenstein_lemma (p : ) [fact (nat.prime p)] [fact (p % 2 = 1)] {a : } (ha1 : a % 2 = 1) (ha0 : a 0) :
= (-1) ^ ∑ (x : ) in (p / 2).succ, x * a / p
theorem zmod.quadratic_reciprocity (p q : ) [fact (nat.prime p)] [fact (nat.prime q)] [hp1 : fact (p % 2 = 1)] [hq1 : fact (q % 2 = 1)] (hpq : p q) :
q) * = (-1) ^ (p / 2) * (q / 2)