# 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

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

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

source
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 #

source
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

Instances For

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

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

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

source
@[simp]
theorem legendreSym.at_zero (p : ℕ) [Fact (Nat.Prime p)] :
legendreSym p 0 = 0
source
@[simp]
theorem legendreSym.at_one (p : ℕ) [Fact (Nat.Prime p)] :
legendreSym p 1 = 1
source
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.

source
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' := ⋯ }

Instances For

source
@[simp]
theorem legendreSym.hom_apply (p : ℕ) [Fact (Nat.Prime p)] (a : ℤ) :
(hom p) a = legendreSym p a
source
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`.

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

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

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

source
theorem legendreSym.eq_one_iff' (p : ℕ) [Fact (Nat.Prime p)] {a : ℕ} (ha0 : ↑a ≠ 0) :
legendreSym p ↑a = 1 ↔ IsSquare ↑a
source
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`.

source
theorem legendreSym.eq_neg_one_iff' (p : ℕ) [Fact (Nat.Prime p)] {a : ℕ} :
legendreSym p ↑a = -1 ↔ ¬IsSquare ↑a
source
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 #

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

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

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

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

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

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

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

source
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