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_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 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) (hap : a ≠ 0) :

multiset.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 : ℕ} (hb0 : 0 < b) (hc : a / b ≤ c) :

a / b = (finset.filter (λ (x : ℕ), x * b ≤ a) (finset.Ico 1 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

zmod.legendre_sym a p = ite (↑a = 0) 0 (ite (↑a ^ (p / 2) = 1) 1 (-1))

theorem zmod.legendre_sym_eq_pow (a p : ℕ) [hp : fact (nat.prime p)] :

↑(zmod.legendre_sym a p) = ↑a ^ (p / 2)

theorem zmod.legendre_sym_eq_one_or_neg_one (a p : ℕ) (ha : ↑a ≠ 0) :

zmod.legendre_sym a p = -1 ∨ zmod.legendre_sym a p = 1

theorem zmod.legendre_sym_eq_zero_iff (a p : ℕ) :

zmod.legendre_sym a p = 0 ↔ ↑a = 0

theorem zmod.gauss_lemma (p : ℕ) [fact (nat.prime p)] {a : ℕ} [fact (p % 2 = 1)] (ha0 : ↑a ≠ 0) :

zmod.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 : ℕ} (ha0 : ↑a ≠ 0) :

zmod.legendre_sym a p = 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) :

zmod.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)] (hpq : p ≠ q) :

(zmod.legendre_sym p q) * zmod.legendre_sym q p = (-1) ^ (p / 2) * (q / 2)

theorem zmod.fact_prime_two :

fact (nat.prime 2)

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_sq_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_sq_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_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) :

(∃ (a : zmod p), a ^ 2 = ↑q) ↔ ¬∃ (b : zmod q), b ^ 2 = ↑p