mathlib documentation

number_theory.quadratic_reciprocity

Quadratic reciprocity.

This file contains results about quadratic residues modulo a prime number.

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_pow_two_eq_prime_iff_of_mod_four_eq_one, and exists_pow_two_eq_prime_iff_of_mod_four_eq_three.

Also proven are conditions for -1 and 2 to be a square modulo a prime, exists_pow_two_eq_neg_one_iff_mod_four_ne_three and exists_pow_two_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} :
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_pow_two_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} :
a 0a ^ (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 finset.Ico 1 p, x = -1

theorem Ico_map_val_min_abs_nat_abs_eq_Ico_map_id (p : ) [hp : fact (nat.prime p)] (a : zmod p) :
a 0multiset.map (λ (x : ), (a * x).val_min_abs.nat_abs) (finset.Ico 1 (p / 2).succ).val = multiset.map (λ (a : ), a) (finset.Ico 1 (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 : } :
0 < ba / b ca / b = (finset.filter (λ (x : ), x * b a) (finset.Ico 1 c.succ)).card

def zmod.legendre_sym  :

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)] :

theorem zmod.gauss_lemma (p : ) [fact (nat.prime p)] {a : } [hp1 : fact (p % 2 = 1)] :
a 0zmod.legendre_sym a p = (-1) ^ (finset.filter (λ (x : ), p / 2 < ((a) * x).val) (finset.Ico 1 (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 : } :
a 0(zmod.legendre_sym a p = 1 ∃ (b : zmod p), b ^ 2 = a)

theorem zmod.eisenstein_lemma (p : ) [fact (nat.prime p)] [hp1 : fact (p % 2 = 1)] {a : } :
a % 2 = 1a 0zmod.legendre_sym a p = (-1) ^ ∑ (x : ) in finset.Ico 1 (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)] :
p q(zmod.legendre_sym p q) * zmod.legendre_sym q p = (-1) ^ (p / 2) * (q / 2)

@[instance]

theorem zmod.legendre_sym_two (p : ) [fact (nat.prime p)] [hp1 : fact (p % 2 = 1)] :
zmod.legendre_sym 2 p = (-1) ^ (p / 4 + p / 2)

theorem zmod.exists_pow_two_eq_two_iff (p : ) [fact (nat.prime p)] [hp1 : fact (p % 2 = 1)] :
(∃ (a : zmod p), a ^ 2 = 2) p % 8 = 1 p % 8 = 7

theorem zmod.exists_pow_two_eq_prime_iff_of_mod_four_eq_one (p q : ) [fact (nat.prime p)] [fact (nat.prime q)] (hp1 : p % 4 = 1) [hq1 : fact (q % 2 = 1)] :
(∃ (a : zmod p), a ^ 2 = q) ∃ (b : zmod q), b ^ 2 = p

theorem zmod.exists_pow_two_eq_prime_iff_of_mod_four_eq_three (p q : ) [fact (nat.prime p)] [fact (nat.prime q)] :
p % 4 = 3q % 4 = 3p q((∃ (a : zmod p), a ^ 2 = q) ¬∃ (b : zmod q), b ^ 2 = p)