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 $\Bigl(\frac{a}{p}\Bigr)$ 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 Legendre symbol is used to define the Jacobi symbol, jacobi_sym a b, for integers a and (odd) natural numbers b, which extends the Legendre symbol.

Main results #

We prove the law of quadratic reciprocity, see legendre_sym.quadratic_reciprocity and legendre_sym.quadratic_reciprocity', as well as the interpretations in terms of existence of square roots depending on the congruence mod 4, zmod.exists_sq_eq_prime_iff_of_mod_four_eq_one, and zmod.exists_sq_eq_prime_iff_of_mod_four_eq_three.

We also prove the supplementary laws that give conditions for when -1 or 2 (or -2) is a square modulo a prime p: legendre_sym.at_neg_one and zmod.exists_sq_eq_neg_one_iff for -1, legendre_sym.at_two and zmod.exists_sq_eq_two_iff for 2, legendre_sym.at_neg_two and zmod.exists_sq_eq_neg_two_iff for -2.

Implementation notes #

The proofs use results for quadratic characters on arbitrary finite fields from number_theory.legendre_symbol.quadratic_char, which in turn are based on properties of quadratic Gauss sums as provided by number_theory.legendre_symbol.gauss_sum.

Tags #

quadratic residue, quadratic nonresidue, Legendre symbol, quadratic reciprocity

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.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

If a : zmod p is nonzero, then a^(p/2) is either 1 or -1.

Definition of the Legendre symbol and basic properties #

def 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 nonzero 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

legendre_sym p a = ⇑(quadratic_char (zmod p)) ↑a

theorem legendre_sym.eq_pow (p : ℕ) [fact (nat.prime p)] (a : ℤ) :

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

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

theorem legendre_sym.eq_one_or_neg_one (p : ℕ) [fact (nat.prime p)] {a : ℤ} (ha : ↑a ≠ 0) :

legendre_sym p a = 1 ∨ legendre_sym p a = -1

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

theorem legendre_sym.eq_neg_one_iff_not_one (p : ℕ) [fact (nat.prime p)] {a : ℤ} (ha : ↑a ≠ 0) :

legendre_sym p a = -1 ↔ ¬legendre_sym p a = 1

theorem legendre_sym.eq_zero_iff (p : ℕ) [fact (nat.prime p)] (a : ℤ) :

legendre_sym p a = 0 ↔ ↑a = 0

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

@[simp]

theorem legendre_sym.at_zero (p : ℕ) [fact (nat.prime p)] :

legendre_sym p 0 = 0

@[simp]

theorem legendre_sym.at_one (p : ℕ) [fact (nat.prime p)] :

legendre_sym p 1 = 1

@[protected]

theorem legendre_sym.mul (p : ℕ) [fact (nat.prime p)] (a b : ℤ) :

legendre_sym p (a * b) = legendre_sym p a * legendre_sym p b

The Legendre symbol is multiplicative in a for p fixed.

@[simp]

theorem legendre_sym.hom_apply (p : ℕ) [fact (nat.prime p)] (a : ℤ) :

⇑(legendre_sym.hom p) a = legendre_sym p a

def legendre_sym.hom (p : ℕ) [fact (nat.prime p)] :

ℤ →*₀ ℤ

The Legendre symbol is a homomorphism of monoids with zero.

Equations

legendre_sym.hom p = {to_fun := legendre_sym p _inst_1, map_zero' := _, map_one' := _, map_mul' := _}

theorem legendre_sym.sq_one (p : ℕ) [fact (nat.prime p)] {a : ℤ} (ha : ↑a ≠ 0) :

legendre_sym p a ^ 2 = 1

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

theorem legendre_sym.sq_one' (p : ℕ) [fact (nat.prime p)] {a : ℤ} (ha : ↑a ≠ 0) :

legendre_sym p (a ^ 2) = 1

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

@[protected]

theorem legendre_sym.mod (p : ℕ) [fact (nat.prime p)] (a : ℤ) :

legendre_sym p a = legendre_sym p (a % ↑p)

The Legendre symbol depends only on a mod p.

theorem legendre_sym.eq_one_iff (p : ℕ) [fact (nat.prime p)] {a : ℤ} (ha0 : ↑a ≠ 0) :

legendre_sym p a = 1 ↔ is_square ↑a

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

theorem legendre_sym.eq_one_iff' (p : ℕ) [fact (nat.prime p)] {a : ℕ} (ha0 : ↑a ≠ 0) :

legendre_sym p ↑a = 1 ↔ is_square ↑a

theorem legendre_sym.eq_neg_one_iff (p : ℕ) [fact (nat.prime p)] {a : ℤ} :

legendre_sym p a = -1 ↔ ¬is_square ↑a

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

theorem legendre_sym.eq_neg_one_iff' (p : ℕ) [fact (nat.prime p)] {a : ℕ} :

legendre_sym p ↑a = -1 ↔ ¬is_square ↑a

theorem legendre_sym.card_sqrts (p : ℕ) [fact (nat.prime p)] (hp : p ≠ 2) (a : ℤ) :

↑({x : zmod p | x ^ 2 = ↑a}.to_finset.card) = legendre_sym p a + 1

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

Applications to binary quadratic forms #

theorem legendre_sym.eq_one_of_sq_sub_mul_sq_eq_zero {p : ℕ} [fact (nat.prime p)] {a : ℤ} (ha : ↑a ≠ 0) {x y : zmod p} (hy : y ≠ 0) (hxy : x ^ 2 - ↑a * y ^ 2 = 0) :

legendre_sym p a = 1

The Legendre symbol legendre_sym p a = 1 if there is a solution in ℤ/pℤ of the equation x^2 - a*y^2 = 0 with y ≠ 0.

theorem legendre_sym.eq_one_of_sq_sub_mul_sq_eq_zero' {p : ℕ} [fact (nat.prime p)] {a : ℤ} (ha : ↑a ≠ 0) {x y : zmod p} (hx : x ≠ 0) (hxy : x ^ 2 - ↑a * y ^ 2 = 0) :

legendre_sym p a = 1

The Legendre symbol legendre_sym p a = 1 if there is a solution in ℤ/pℤ of the equation x^2 - a*y^2 = 0 with x ≠ 0.

theorem legendre_sym.eq_zero_mod_of_eq_neg_one {p : ℕ} [fact (nat.prime p)] {a : ℤ} (h : legendre_sym p a = -1) {x y : zmod p} (hxy : x ^ 2 - ↑a * y ^ 2 = 0) :

x = 0 ∧ y = 0

If legendre_sym p a = -1, then the only solution of x^2 - a*y^2 = 0 in ℤ/pℤ is the trivial one.

theorem legendre_sym.prime_dvd_of_eq_neg_one {p : ℕ} [fact (nat.prime p)] {a : ℤ} (h : legendre_sym p a = -1) {x y : ℤ} (hxy : ↑p ∣ x ^ 2 - a * y ^ 2) :

↑p ∣ x ∧ ↑p ∣ y

If legendre_sym p a = -1 and p divides x^2 - a*y^2, then p must divide x and y.

The value of the Legendre symbol at `-1` #

See jacobi_sym.at_neg_one for the corresponding statement for the Jacobi symbol.

theorem legendre_sym.at_neg_one {p : ℕ} [fact (nat.prime p)] (hp : p ≠ 2) :

legendre_sym p (-1) = ⇑zmod.χ₄ ↑p

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

theorem zmod.exists_sq_eq_neg_one_iff {p : ℕ} [fact (nat.prime p)] :

is_square (-1) ↔ p % 4 ≠ 3

-1 is a square in zmod p iff p is not congruent to 3 mod 4.

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

If two nonzero squares are negatives of each other in zmod p, then 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

The value of the Legendre symbol at `2` and `-2` #

See jacobi_sym.at_two and jacobi_sym.at_neg_two for the corresponding statements for the Jacobi symbol.

theorem legendre_sym.at_two {p : ℕ} [fact (nat.prime p)] (hp : p ≠ 2) :

legendre_sym p 2 = ⇑zmod.χ₈ ↑p

legendre_sym p 2 is given by χ₈ p.

theorem legendre_sym.at_neg_two {p : ℕ} [fact (nat.prime p)] (hp : p ≠ 2) :

legendre_sym p (-2) = ⇑zmod.χ₈' ↑p

legendre_sym p (-2) is given by χ₈' p.

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

is_square 2 ↔ p % 8 = 1 ∨ p % 8 = 7

2 is a square modulo an odd prime p iff p is congruent to 1 or 7 mod 8.

theorem zmod.exists_sq_eq_neg_two_iff {p : ℕ} [fact (nat.prime p)] (hp : p ≠ 2) :

is_square (-2) ↔ p % 8 = 1 ∨ p % 8 = 3

-2 is a square modulo an odd prime p iff p is congruent to 1 or 3 mod 8.

The Law of Quadratic Reciprocity #

See jacobi_sym.quadratic_reciprocity and variants for a version of Quadratic Reciprocity for the Jacobi symbol.

theorem legendre_sym.quadratic_reciprocity {p q : ℕ} [fact (nat.prime p)] [fact (nat.prime q)] (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) :

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

The Law of Quadratic Reciprocity: if p and q are distinct odd primes, then (q / p) * (p / q) = (-1)^((p-1)(q-1)/4).

theorem legendre_sym.quadratic_reciprocity' {p q : ℕ} [fact (nat.prime p)] [fact (nat.prime q)] (hp : p ≠ 2) (hq : q ≠ 2) :

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

The Law of Quadratic Reciprocity: if p and q are odd primes, then (q / p) = (-1)^((p-1)(q-1)/4) * (p / q).

theorem legendre_sym.quadratic_reciprocity_one_mod_four {p q : ℕ} [fact (nat.prime p)] [fact (nat.prime q)] (hp : p % 4 = 1) (hq : q ≠ 2) :

legendre_sym q ↑p = legendre_sym p ↑q

The Law of Quadratic Reciprocity: if p and q are odd primes and p % 4 = 1, then (q / p) = (p / q).

theorem legendre_sym.quadratic_reciprocity_three_mod_four {p q : ℕ} [fact (nat.prime p)] [fact (nat.prime q)] (hp : p % 4 = 3) (hq : q % 4 = 3) :

legendre_sym q ↑p = -legendre_sym p ↑q

The Law of Quadratic Reciprocity: if p and q are primes that are both congruent to 3 mod 4, then (q / p) = -(p / q).

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

is_square ↑q ↔ is_square ↑p

If p and q are odd primes and p % 4 = 1, then q is a square mod p iff p is a square mod q.

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

is_square ↑q ↔ ¬is_square ↑p

If p and q are distinct primes that are both congruent to 3 mod 4, then q is a square mod p iff p is a nonsquare mod q.