mathlib documentation

number_theory.legendre_symbol.quadratic_reciprocity

Legendre symbol and 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, legende_sym_neg_one and exists_sq_eq_neg_one_iff for -1, and exists_sq_eq_two_iff for 2

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) :
is_square 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.mod_four_ne_three_of_sq_eq_neg_one (p : ) [fact (nat.prime p)] {y : zmod p} (hy : y ^ 2 = -1) :
p % 4 3
theorem zmod.mod_four_ne_three_of_sq_eq_neg_sq' (p : ) [fact (nat.prime p)] {x y : zmod p} (hy : y 0) (hxy : x ^ 2 = -y ^ 2) :
p % 4 3
theorem zmod.mod_four_ne_three_of_sq_eq_neg_sq (p : ) [fact (nat.prime p)] {x y : zmod p} (hx : x 0) (hxy : x ^ 2 = -y ^ 2) :
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 : ) [fact (nat.prime p)] (a : ) :

The Legendre symbol of a : ℤ and a prime p, legendre_sym p a, is an integer defined as

  • 0 if a is 0 modulo p;
  • 1 if 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
theorem zmod.legendre_sym_eq_pow (p : ) (a : ) [hp : fact (nat.prime p)] :

We have the congruence legendre_sym p a ≡ a ^ (p / 2) mod p.

If p ∤ a, then legendre_sym p a is 1 or -1.

theorem zmod.legendre_sym_eq_zero_iff (p : ) [fact (nat.prime p)] (a : ) :

The Legendre symbol of p and a is zero iff p ∣ a.

@[simp]
@[simp]

The Legendre symbol is multiplicative in a for p fixed.

The Legendre symbol is a homomorphism of monoids with zero.

Equations
theorem zmod.legendre_sym_sq_one (p : ) [fact (nat.prime p)] (a : ) (ha : a 0) :

The square of the symbol is 1 if p ∤ a.

theorem zmod.legendre_sym_sq_one' (p : ) [fact (nat.prime p)] (a : ) (ha : a 0) :

The Legendre symbol of a^2 at p is 1 if p ∤ a.

The Legendre symbol depends only on a mod p.

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

When p ∤ a, then legendre_sym p a = 1 iff a is a square mod p.

legendre_sym p a = -1 iffa is a nonsquare mod p.

theorem zmod.legendre_sym_card_sqrts (p : ) [fact (nat.prime p)] (hp : p 2) (a : ) :
({x : zmod p | x ^ 2 = a}.to_finset.card) = zmod.legendre_sym p a + 1

The number of square roots of a modulo p is determined by the Legendre symbol.

theorem zmod.legendre_sym_neg_one (p : ) [fact (nat.prime p)] (hp : p 2) :

legendre_sym p (-1) is given by χ₄ p.

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) ^ (finset.Ico 1 (p / 2).succ).sum (λ (x : ), 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) :
is_square 2 p % 8 = 1 p % 8 = 7
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) :