# mathlib3documentation

number_theory.legendre_symbol.basic

# Legendre symbol #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains results about Legendre symbols.

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 also prove the supplementary laws that give conditions for when -1 is a square modulo a prime p: legendre_sym.at_neg_one and zmod.exists_sq_eq_neg_one_iff for -1.

See number_theory.legendre_symbol.quadratic_reciprocity for the conditions when 2 and -2 are squares: 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.

## Tags #

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) :
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
theorem legendre_sym.eq_pow (p : ) [fact (nat.prime p)] (a : ) :
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) :
a = 1 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) :
a = -1 ¬ a = 1
theorem legendre_sym.eq_zero_iff (p : ) [fact (nat.prime p)] (a : ) :
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)] :
0 = 0
@[simp]
theorem legendre_sym.at_one (p : ) [fact (nat.prime p)] :
1 = 1
@[protected]
theorem legendre_sym.mul (p : ) [fact (nat.prime p)] (a b : ) :
(a * b) = a * b

The Legendre symbol is multiplicative in a for p fixed.

@[simp]
theorem legendre_sym.hom_apply (p : ) [fact (nat.prime p)] (a : ) :
a = a
def legendre_sym.hom (p : ) [fact (nat.prime p)] :

The Legendre symbol is a homomorphism of monoids with zero.

Equations
theorem legendre_sym.sq_one (p : ) [fact (nat.prime p)] {a : } (ha : a 0) :
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) :
(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 : ) :
a = (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) :
a = 1

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) :
= 1
theorem legendre_sym.eq_neg_one_iff (p : ) [fact (nat.prime p)] {a : } :
a = -1

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 : } :
= -1
theorem legendre_sym.card_sqrts (p : ) [fact (nat.prime p)] (hp : p 2) (a : ) :
({x : zmod p | x ^ 2 = a}.to_finset.card) = 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) :
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) :
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 : 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 : 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) :
(-1) =

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