Legendre symbol

This file contains results about Legendre symbols.

We define the Legendre symbol $\Bigl(\frac{a}{p}\Bigr)$ as legendreSym p a. Note the order of arguments! The advantage of this form is that then legendreSym p is a multiplicative map.

The Legendre symbol is used to define the Jacobi symbol, jacobiSym 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: legendreSym.at_neg_one and ZMod.exists_sq_eq_neg_one_iff for -1.

See NumberTheory.LegendreSymbol.QuadraticReciprocity for the conditions when 2 and -2 are squares: legendreSym.at_two and ZMod.exists_sq_eq_two_iff for 2, legendreSym.at_neg_two and ZMod.exists_sq_eq_neg_two_iff for -2.

Tags

quadratic residue, quadratic nonresidue, Legendre symbol

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) : IsSquare 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 legendreSym (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ) : ℤ

The Legendre symbol of a : ℤ and a prime p, legendreSym 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 legendreSym p is a multiplicative function ℤ → ℤ.

Equations

• legendreSym p a = (quadraticChar (ZMod p)) ↑a

theorem legendreSym.eq_pow (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ) : ↑(legendreSym p a) = ↑a ^ (p / 2)

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

theorem legendreSym.eq_one_or_neg_one (p : ℕ) [Fact (Nat.Prime p)] {a : ℤ} (ha : ↑a ≠ 0) : legendreSym p a = 1 ∨ legendreSym p a = -1

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

theorem legendreSym.eq_neg_one_iff_not_one (p : ℕ) [Fact (Nat.Prime p)] {a : ℤ} (ha : ↑a ≠ 0) : legendreSym p a = -1 ↔ ¬legendreSym p a = 1

theorem legendreSym.eq_zero_iff (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ) : legendreSym p a = 0 ↔ ↑a = 0

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

@[simp]

theorem legendreSym.at_zero (p : ℕ) [Fact (Nat.Prime p)] : legendreSym p 0 = 0

@[simp]

theorem legendreSym.at_one (p : ℕ) [Fact (Nat.Prime p)] : legendreSym p 1 = 1

theorem legendreSym.mul (p : ℕ) [Fact (Nat.Prime p)] (a b : ℤ) : legendreSym p (a * b) = legendreSym p a * legendreSym p b

The Legendre symbol is multiplicative in a for p fixed.

def legendreSym.hom (p : ℕ) [Fact (Nat.Prime p)] : ℤ →*₀ ℤ

The Legendre symbol is a homomorphism of monoids with zero.

Equations

• legendreSym.hom p = { toFun := legendreSym p, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem legendreSym.hom_apply (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ) : (legendreSym.hom p) a = legendreSym p a

theorem legendreSym.sq_one (p : ℕ) [Fact (Nat.Prime p)] {a : ℤ} (ha : ↑a ≠ 0) : legendreSym p a ^ 2 = 1

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

theorem legendreSym.sq_one' (p : ℕ) [Fact (Nat.Prime p)] {a : ℤ} (ha : ↑a ≠ 0) : legendreSym p (a ^ 2) = 1

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

theorem legendreSym.mod (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ) : legendreSym p a = legendreSym p (a % ↑p)

The Legendre symbol depends only on a mod p.

theorem legendreSym.eq_one_iff (p : ℕ) [Fact (Nat.Prime p)] {a : ℤ} (ha0 : ↑a ≠ 0) : legendreSym p a = 1 ↔ IsSquare ↑a

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

theorem legendreSym.eq_one_iff' (p : ℕ) [Fact (Nat.Prime p)] {a : ℕ} (ha0 : ↑a ≠ 0) : legendreSym p ↑a = 1 ↔ IsSquare ↑a

theorem legendreSym.eq_neg_one_iff (p : ℕ) [Fact (Nat.Prime p)] {a : ℤ} : legendreSym p a = -1 ↔ ¬IsSquare ↑a

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

theorem legendreSym.eq_neg_one_iff' (p : ℕ) [Fact (Nat.Prime p)] {a : ℕ} : legendreSym p ↑a = -1 ↔ ¬IsSquare ↑a

theorem legendreSym.card_sqrts (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (a : ℤ) : ↑{x : ZMod p | x ^ 2 = ↑a}.toFinset.card = legendreSym p a + 1

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

Applications to binary quadratic forms

theorem legendreSym.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) : legendreSym p a = 1

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

theorem legendreSym.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) : legendreSym p a = 1

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

theorem legendreSym.eq_zero_mod_of_eq_neg_one {p : ℕ} [Fact (Nat.Prime p)] {a : ℤ} (h : legendreSym p a = -1) {x y : ZMod p} (hxy : x ^ 2 - ↑a * y ^ 2 = 0) : x = 0 ∧ y = 0

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

theorem legendreSym.prime_dvd_of_eq_neg_one {p : ℕ} [Fact (Nat.Prime p)] {a : ℤ} (h : legendreSym p a = -1) {x y : ℤ} (hxy : ↑p ∣ x ^ 2 - a * y ^ 2) : ↑p ∣ x ∧ ↑p ∣ y

If legendreSym 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 jacobiSym.at_neg_one for the corresponding statement for the Jacobi symbol.

theorem legendreSym.at_neg_one {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) : legendreSym p (-1) = ZMod.χ₄ ↑p

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

theorem ZMod.exists_sq_eq_neg_one_iff {p : ℕ} [Fact (Nat.Prime p)] : IsSquare (-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