Documentation

Mathlib.NumberTheory.LegendreSymbol.Basic

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
šŸ“ coverage
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
šŸ“ coverage
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
šŸ“ coverage
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
šŸ”ø coverage
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 ā„¤ ā†’ ā„¤.

Instances For
    source
    šŸ“ coverage
    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
    šŸ“ coverage
    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
    šŸ“ coverage
    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
    šŸ“ coverage
    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
    šŸ“ coverage
    @[simp]
    theorem legendreSym.at_zero (p : ā„•) [Fact (Nat.Prime p)] :
    legendreSym p 0 = 0
    source
    šŸ“ coverage
    @[simp]
    theorem legendreSym.at_one (p : ā„•) [Fact (Nat.Prime p)] :
    legendreSym p 1 = 1
    source
    šŸ“ coverage
    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
    šŸ”ø coverage
    def legendreSym.hom (p : ā„•) [Fact (Nat.Prime p)] :
    ā„¤ ā†’*ā‚€ ā„¤

    The Legendre symbol is a homomorphism of monoids with zero.

    Instances For
      source
      šŸ“ coverage
      @[simp]
      theorem legendreSym.hom_apply (p : ā„•) [Fact (Nat.Prime p)] (a : ā„¤) :
      (hom p) a = legendreSym p a
      source
      šŸ“ coverage
      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
      šŸ“ coverage
      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
      šŸ“ coverage
      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
      šŸ“ coverage
      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
      šŸ“ coverage
      theorem legendreSym.eq_one_iff' (p : ā„•) [Fact (Nat.Prime p)] {a : ā„•} (ha0 : ā†‘a ā‰  0) :
      legendreSym p ā†‘a = 1 ā†” IsSquare ā†‘a
      source
      šŸ“ coverage
      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
      šŸ“ coverage
      theorem legendreSym.eq_neg_one_iff' (p : ā„•) [Fact (Nat.Prime p)] {a : ā„•} :
      legendreSym p ā†‘a = -1 ā†” Ā¬IsSquare ā†‘a
      source
      šŸ“ coverage
      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
      šŸ“ coverage
      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
      šŸ“ coverage
      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
      šŸ“ coverage
      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
      šŸ“ coverage
      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
      šŸ“ coverage
      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