# mathlib3documentation

number_theory.legendre_symbol.jacobi_symbol

# The Jacobi Symbol #

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

We define the Jacobi symbol and prove its main properties.

## Main definitions #

We define the Jacobi symbol, jacobi_sym a b, for integers a and natural numbers b as the product over the prime factors p of b of the Legendre symbols legendre_sym 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 jacobi_sym a 0 = 1 for all a.

## Main statements #

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

• Multiplicativity in both arguments (jacobi_sym.mul_left, jacobi_sym.mul_right)

• The value of the symbol is 1 or -1 when the arguments are coprime (jacobi_sym.eq_one_or_neg_one)

• The symbol vanishes if and only if b ≠ 0 and the arguments are not coprime (jacobi_sym.eq_zero_iff)

• If the symbol has the value -1, then a : zmod b is not a square (zmod.nonsquare_of_jacobi_sym_eq_neg_one); the converse holds when b = p is a prime (zmod.nonsquare_iff_jacobi_sym_eq_neg_one); in particular, in this case a is a square mod p when the symbol has the value 1 (zmod.is_square_of_jacobi_sym_eq_one).

• Quadratic reciprocity (jacobi_sym.quadratic_reciprocity, jacobi_sym.quadratic_reciprocity_one_mod_four, jacobi_sym.quadratic_reciprocity_three_mod_four)

• The supplementary laws for a = -1, a = 2, a = -2 (jacobi_sym.at_neg_one, jacobi_sym.at_two, jacobi_sym.at_neg_two)

• The symbol depends on a only via its residue class mod b (jacobi_sym.mod_left) and on b only via its residue class mod 4*a (jacobi_sym.mod_right)

## Notations #

We define the notation J(a | b) for jacobi_sym a b, localized to number_theory_symbols.

## Tags #

### 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 jacobi_sym a b.

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

def jacobi_sym (a : ) (b : ) :

The Jacobi symbol of a and b

Equations

### Properties of the Jacobi symbol #

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

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

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

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

theorem legendre_sym.to_jacobi_sym (p : ) [fp : fact (nat.prime p)] (a : ) :
a = p

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

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

The Jacobi symbol is multiplicative in its second argument.

theorem jacobi_sym.mul_right (a : ) (b₁ b₂ : ) [ne_zero b₁] [ne_zero b₂] :
(b₁ * b₂) = b₁ * b₂

The Jacobi symbol is multiplicative in its second argument.

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

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

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

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

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

The Jacobi symbol is multiplicative in its first argument.

theorem jacobi_sym.eq_zero_iff_not_coprime {a : } {b : } [ne_zero b] :
b = 0 a.gcd b 1

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

@[protected]
theorem jacobi_sym.ne_zero {a : } {b : } (h : a.gcd b = 1) :
b 0

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

theorem jacobi_sym.eq_zero_iff {a : } {b : } :
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 jacobi_sym.zero_left {b : } (hb : 1 < b) :
b = 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem jacobi_sym.prime_dvd_of_eq_neg_one {p : } [fact (nat.prime p)] {a : } (h : 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 jacobi_sym.list_prod_left {l : list } {n : } :
n = (list.map (λ (a : ), n) l).prod

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

theorem jacobi_sym.list_prod_right {a : } {l : list } (hl : (n : ), n l n 0) :
l.prod = (list.map (λ (n : ), n) l).prod

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

theorem jacobi_sym.eq_neg_one_at_prime_divisor_of_eq_neg_one {a : } {n : } (h : n = -1) :
(p : ) (hp : , p n p = -1

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

theorem zmod.nonsquare_of_jacobi_sym_eq_neg_one {a : } {b : } (h : b = -1) :

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

theorem zmod.nonsquare_iff_jacobi_sym_eq_neg_one {a : } {p : } [fact (nat.prime p)] :
p = -1

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

theorem zmod.is_square_of_jacobi_sym_eq_one {a : } {p : } [fact (nat.prime p)] (h : p = 1) :

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

### Values at -1, 2 and -2#

theorem jacobi_sym.value_at (a : ) {R : Type u_1} (χ : R →* ) (hp : (p : ) (pp : , p 2 a = χ p) {b : } (hb : odd b) :
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 jacobi_sym.at_neg_one {b : } (hb : odd b) :
jacobi_sym (-1) b =

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

@[protected]
theorem jacobi_sym.neg (a : ) {b : } (hb : odd b) :
jacobi_sym (-a) b = * b

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

theorem jacobi_sym.at_two {b : } (hb : odd b) :
b =

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

theorem jacobi_sym.at_neg_two {b : } (hb : odd b) :
jacobi_sym (-2) b =

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

def qr_sign (m n : ) :

Equations
• n = n
theorem qr_sign.neg_one_pow {m n : } (hm : odd m) (hn : odd n) :
n = (-1) ^ (m / 2 * (n / 2))

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

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

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

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

qr_sign is multiplicative in the first argument.

theorem qr_sign.mul_right (m n₁ n₂ : ) [ne_zero n₁] [ne_zero n₂] :
(n₁ * n₂) = n₁ * n₂

qr_sign is multiplicative in the second argument.

@[protected]
theorem qr_sign.symm {m n : } (hm : odd m) (hn : odd n) :
n = m

qr_sign is symmetric when both arguments are odd.

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

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

theorem jacobi_sym.quadratic_reciprocity' {a b : } (ha : odd a) (hb : odd b) :
b = a * a

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

theorem jacobi_sym.quadratic_reciprocity {a b : } (ha : odd a) (hb : odd b) :
b = (-1) ^ (a / 2 * (b / 2)) * a

The Law of Quadratic Reciprocity for the Jacobi symbol

theorem jacobi_sym.quadratic_reciprocity_one_mod_four {a b : } (ha : a % 4 = 1) (hb : odd b) :
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 jacobi_sym.quadratic_reciprocity_one_mod_four' {a b : } (ha : odd a) (hb : b % 4 = 1) :
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 jacobi_sym.quadratic_reciprocity_three_mod_four {a b : } (ha : a % 4 = 3) (hb : b % 4 = 3) :
b = - a

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

theorem jacobi_sym.mod_right' (a : ) {b : } (hb : odd b) :
b = (b % (4 * a))

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

theorem jacobi_sym.mod_right (a : ) {b : } (hb : odd b) :
b = (b % (4 * a.nat_abs))

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