Documentation

Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

The Jacobi Symbol #

We define the Jacobi symbol and prove its main properties.

Main definitions #

We define the Jacobi symbol, jacobiSym a b, for integers a and natural numbers b as the product over the prime factors p of b of the Legendre symbols legendreSym p a. This agrees with the mathematical definition when b is odd.

The prime factors are obtained via Nat.factors. Since Nat.factors 0 = [], this implies in particular that jacobiSym a 0 = 1 for all a.

Main statements #

We prove the main properties of the Jacobi symbol, including the following.

Notations #

We define the notation J(a | b) for jacobiSym a b, localized to NumberTheorySymbols.

Tags #

Jacobi symbol, quadratic reciprocity

Definition of the Jacobi symbol #

We define the Jacobi symbol $\Bigl(\frac{a}{b}\Bigr)$ for integers a and natural numbers b as the product of the Legendre symbols $\Bigl(\frac{a}{p}\Bigr)$, where p runs through the prime divisors (with multiplicity) of b, as provided by b.factors. This agrees with the Jacobi symbol when b is odd and gives less meaningful values when it is not (e.g., the symbol is 1 when b = 0). This is called jacobiSym a b.

We define localized notation (locale NumberTheorySymbols) J(a | b) for the Jacobi symbol jacobiSym a b.

def jacobiSym (a : ) (b : ) :

The Jacobi symbol of a and b

Equations
Instances For

    The Jacobi symbol of a and b

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Properties of the Jacobi symbol #

      @[simp]
      theorem jacobiSym.zero_right (a : ) :
      jacobiSym a 0 = 1

      The symbol J(a | 0) has the value 1.

      @[simp]
      theorem jacobiSym.one_right (a : ) :
      jacobiSym a 1 = 1

      The symbol J(a | 1) has the value 1.

      The Legendre symbol legendreSym p a with an integer a and a prime number p is the same as the Jacobi symbol J(a | p).

      theorem jacobiSym.mul_right' (a : ) {b₁ : } {b₂ : } (hb₁ : b₁ 0) (hb₂ : b₂ 0) :
      jacobiSym a (b₁ * b₂) = jacobiSym a b₁ * jacobiSym a b₂

      The Jacobi symbol is multiplicative in its second argument.

      theorem jacobiSym.mul_right (a : ) (b₁ : ) (b₂ : ) [NeZero b₁] [NeZero b₂] :
      jacobiSym a (b₁ * b₂) = jacobiSym a b₁ * jacobiSym a b₂

      The Jacobi symbol is multiplicative in its second argument.

      theorem jacobiSym.trichotomy (a : ) (b : ) :
      jacobiSym a b = 0 jacobiSym a b = 1 jacobiSym a b = -1

      The Jacobi symbol takes only the values 0, 1 and -1.

      @[simp]
      theorem jacobiSym.one_left (b : ) :
      jacobiSym 1 b = 1

      The symbol J(1 | b) has the value 1.

      theorem jacobiSym.mul_left (a₁ : ) (a₂ : ) (b : ) :
      jacobiSym (a₁ * a₂) b = jacobiSym a₁ b * jacobiSym a₂ b

      The Jacobi symbol is multiplicative in its first argument.

      theorem jacobiSym.eq_zero_iff_not_coprime {a : } {b : } [NeZero b] :
      jacobiSym a b = 0 a.gcd b 1

      The symbol J(a | b) vanishes iff a and b are not coprime (assuming b ≠ 0).

      theorem jacobiSym.ne_zero {a : } {b : } (h : a.gcd b = 1) :

      The symbol J(a | b) is nonzero when a and b are coprime.

      theorem jacobiSym.eq_zero_iff {a : } {b : } :
      jacobiSym a b = 0 b 0 a.gcd b 1

      The symbol J(a | b) vanishes if and only if b ≠ 0 and a and b are not coprime.

      theorem jacobiSym.zero_left {b : } (hb : 1 < b) :
      jacobiSym 0 b = 0

      The symbol J(0 | b) vanishes when b > 1.

      theorem jacobiSym.eq_one_or_neg_one {a : } {b : } (h : a.gcd b = 1) :
      jacobiSym a b = 1 jacobiSym a b = -1

      The symbol J(a | b) takes the value 1 or -1 if a and b are coprime.

      theorem jacobiSym.pow_left (a : ) (e : ) (b : ) :
      jacobiSym (a ^ e) b = jacobiSym a b ^ e

      We have that J(a^e | b) = J(a | b)^e.

      theorem jacobiSym.pow_right (a : ) (b : ) (e : ) :
      jacobiSym a (b ^ e) = jacobiSym a b ^ e

      We have that J(a | b^e) = J(a | b)^e.

      theorem jacobiSym.sq_one {a : } {b : } (h : a.gcd b = 1) :
      jacobiSym a b ^ 2 = 1

      The square of J(a | b) is 1 when a and b are coprime.

      theorem jacobiSym.sq_one' {a : } {b : } (h : a.gcd b = 1) :
      jacobiSym (a ^ 2) b = 1

      The symbol J(a^2 | b) is 1 when a and b are coprime.

      theorem jacobiSym.mod_left (a : ) (b : ) :
      jacobiSym a b = jacobiSym (a % b) b

      The symbol J(a | b) depends only on a mod b.

      theorem jacobiSym.mod_left' {a₁ : } {a₂ : } {b : } (h : a₁ % b = a₂ % b) :
      jacobiSym a₁ b = jacobiSym a₂ b

      The symbol J(a | b) depends only on a mod b.

      theorem jacobiSym.prime_dvd_of_eq_neg_one {p : } [Fact (Nat.Prime p)] {a : } (h : jacobiSym a p = -1) {x : } {y : } (hxy : p x ^ 2 - a * y ^ 2) :
      p x p y

      If p is prime, J(a | p) = -1 and p divides x^2 - a*y^2, then p must divide x and y.

      theorem jacobiSym.list_prod_left {l : List } {n : } :
      jacobiSym l.prod n = (List.map (fun (a : ) => jacobiSym a n) l).prod

      We can pull out a product over a list in the first argument of the Jacobi symbol.

      theorem jacobiSym.list_prod_right {a : } {l : List } (hl : nl, n 0) :
      jacobiSym a l.prod = (List.map (fun (n : ) => jacobiSym a n) l).prod

      We can pull out a product over a list in the second argument of the Jacobi symbol.

      theorem jacobiSym.eq_neg_one_at_prime_divisor_of_eq_neg_one {a : } {n : } (h : jacobiSym a n = -1) :
      ∃ (p : ), Nat.Prime p p n jacobiSym a p = -1

      If J(a | n) = -1, then n has a prime divisor p such that J(a | p) = -1.

      theorem ZMod.nonsquare_of_jacobiSym_eq_neg_one {a : } {b : } (h : jacobiSym a b = -1) :

      If J(a | b) is -1, then a is not a square modulo b.

      If p is prime, then J(a | p) is -1 iff a is not a square modulo p.

      theorem ZMod.isSquare_of_jacobiSym_eq_one {a : } {p : } [Fact (Nat.Prime p)] (h : jacobiSym a p = 1) :

      If p is prime and J(a | p) = 1, then a is a square mod p.

      Values at -1, 2 and -2 #

      theorem jacobiSym.value_at (a : ) {R : Type u_1} [CommSemiring R] (χ : R →* ) (hp : ∀ (p : ) (pp : Nat.Prime p), p 2legendreSym p a = χ p) {b : } (hb : Odd b) :
      jacobiSym a b = χ b

      If χ is a multiplicative function such that J(a | p) = χ p for all odd primes p, then J(a | b) equals χ b for all odd natural numbers b.

      theorem jacobiSym.at_neg_one {b : } (hb : Odd b) :
      jacobiSym (-1) b = ZMod.χ₄ b

      If b is odd, then J(-1 | b) is given by χ₄ b.

      theorem jacobiSym.neg (a : ) {b : } (hb : Odd b) :
      jacobiSym (-a) b = ZMod.χ₄ b * jacobiSym a b

      If b is odd, then J(-a | b) = χ₄ b * J(a | b).

      theorem jacobiSym.at_two {b : } (hb : Odd b) :
      jacobiSym 2 b = ZMod.χ₈ b

      If b is odd, then J(2 | b) is given by χ₈ b.

      theorem jacobiSym.at_neg_two {b : } (hb : Odd b) :
      jacobiSym (-2) b = ZMod.χ₈' b

      If b is odd, then J(-2 | b) is given by χ₈' b.

      theorem jacobiSym.div_four_left {a : } {b : } (ha4 : a % 4 = 0) (hb2 : b % 2 = 1) :
      jacobiSym (a / 4) b = jacobiSym a b
      theorem jacobiSym.even_odd {a : } {b : } (ha2 : a % 2 = 0) (hb2 : b % 2 = 1) :
      (if b % 8 = 3 b % 8 = 5 then -jacobiSym (a / 2) b else jacobiSym (a / 2) b) = jacobiSym a b

      Quadratic Reciprocity #

      def qrSign (m : ) (n : ) :

      The bi-multiplicative map giving the sign in the Law of Quadratic Reciprocity

      Equations
      Instances For
        theorem qrSign.neg_one_pow {m : } {n : } (hm : Odd m) (hn : Odd n) :
        qrSign m n = (-1) ^ (m / 2 * (n / 2))

        We can express qrSign m n as a power of -1 when m and n are odd.

        theorem qrSign.sq_eq_one {m : } {n : } (hm : Odd m) (hn : Odd n) :
        qrSign m n ^ 2 = 1

        When m and n are odd, then the square of qrSign m n is 1.

        theorem qrSign.mul_left (m₁ : ) (m₂ : ) (n : ) :
        qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n

        qrSign is multiplicative in the first argument.

        theorem qrSign.mul_right (m : ) (n₁ : ) (n₂ : ) [NeZero n₁] [NeZero n₂] :
        qrSign m (n₁ * n₂) = qrSign m n₁ * qrSign m n₂

        qrSign is multiplicative in the second argument.

        theorem qrSign.symm {m : } {n : } (hm : Odd m) (hn : Odd n) :
        qrSign m n = qrSign n m

        qrSign is symmetric when both arguments are odd.

        theorem qrSign.eq_iff_eq {m : } {n : } (hm : Odd m) (hn : Odd n) (x : ) (y : ) :
        qrSign m n * x = y x = qrSign m n * y

        We can move qrSign m n from one side of an equality to the other when m and n are odd.

        theorem jacobiSym.quadratic_reciprocity' {a : } {b : } (ha : Odd a) (hb : Odd b) :
        jacobiSym (↑a) b = qrSign b a * jacobiSym (↑b) a

        The Law of Quadratic Reciprocity for the Jacobi symbol, version with qrSign

        theorem jacobiSym.quadratic_reciprocity {a : } {b : } (ha : Odd a) (hb : Odd b) :
        jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a

        The Law of Quadratic Reciprocity for the Jacobi symbol

        theorem jacobiSym.quadratic_reciprocity_one_mod_four {a : } {b : } (ha : a % 4 = 1) (hb : Odd b) :
        jacobiSym (↑a) b = jacobiSym (↑b) a

        The Law of Quadratic Reciprocity for the Jacobi symbol: if a and b are natural numbers with a % 4 = 1 and b odd, then J(a | b) = J(b | a).

        theorem jacobiSym.quadratic_reciprocity_one_mod_four' {a : } {b : } (ha : Odd a) (hb : b % 4 = 1) :
        jacobiSym (↑a) b = jacobiSym (↑b) a

        The Law of Quadratic Reciprocity for the Jacobi symbol: if a and b are natural numbers with a odd and b % 4 = 1, then J(a | b) = J(b | a).

        theorem jacobiSym.quadratic_reciprocity_three_mod_four {a : } {b : } (ha : a % 4 = 3) (hb : b % 4 = 3) :
        jacobiSym (↑a) b = -jacobiSym (↑b) a

        The Law of Quadratic Reciprocity for the Jacobi symbol: if a and b are natural numbers both congruent to 3 mod 4, then J(a | b) = -J(b | a).

        theorem jacobiSym.quadratic_reciprocity_if {a : } {b : } (ha2 : a % 2 = 1) (hb2 : b % 2 = 1) :
        (if a % 4 = 3 b % 4 = 3 then -jacobiSym (↑b) a else jacobiSym (↑b) a) = jacobiSym (↑a) b
        theorem jacobiSym.mod_right' (a : ) {b : } (hb : Odd b) :
        jacobiSym (↑a) b = jacobiSym (↑a) (b % (4 * a))

        The Jacobi symbol J(a | b) depends only on b mod 4*a (version for a : ℕ).

        theorem jacobiSym.mod_right (a : ) {b : } (hb : Odd b) :
        jacobiSym a b = jacobiSym a (b % (4 * a.natAbs))

        The Jacobi symbol J(a | b) depends only on b mod 4*a.

        Fast computation of the Jacobi symbol #

        We follow the implementation as in Mathlib.Tactic.NormNum.LegendreSymbol.