mathlib documentation

number_theory.legendre_symbol.quadratic_reciprocity

Quadratic reciprocity. #

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

We define the Legendre symbol (a / p) as legendre_sym p a. Note the order of arguments! The advantage of this form is that then legendre_sym p is a multiplicative map.

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 : (zmod p)ˣ) :

(∃ (y : (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

def zmod.legendre_sym (p : ℕ) (a : ℤ) :

The Legendre symbol of a and p, legendre_sym p a, 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.

Note the order of the arguments! The advantage of the order chosen here is that legendre_sym p is a multiplicative function ℤ → ℤ.

Equations

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

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

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

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

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

theorem zmod.legendre_sym_eq_zero_iff (p : ℕ) (a : ℤ) :

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

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

zmod.legendre_sym p a = (-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 p a = 1 ↔ ∃ (b : zmod p), b ^ 2 = ↑a

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

zmod.legendre_sym p ↑a = (-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 : p ≠ 2) (hq1 : q ≠ 2) (hpq : p ≠ q) :

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

Quadratic reciprocity theorem

theorem zmod.legendre_sym_two (p : ℕ) [fact (nat.prime p)] (hp2 : p ≠ 2) :

zmod.legendre_sym p 2 = (-1) ^ (p / 4 + p / 2)

theorem zmod.exists_sq_eq_two_iff (p : ℕ) [fact (nat.prime p)] (hp1 : p ≠ 2) :

(∃ (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 : q ≠ 2) :

(∃ (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