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

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

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

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

• If the symbol has the value -1, then a : ZMod b is not a square (ZMod.nonsquare_of_jacobiSym_eq_neg_one); the converse holds when b = p is a prime (ZMod.nonsquare_iff_jacobiSym_eq_neg_one); in particular, in this case a is a square mod p when the symbol has the value 1 (ZMod.isSquare_of_jacobiSym_eq_one).

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

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

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

• A csimp rule for jacobiSym and legendreSym that evaluates J(a | b) efficiently by reducing to the case 0 ≤ a < b and a, b odd, and then swaps a, b and recurses using quadratic reciprocity.

## Notations #

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

## 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 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
• = (List.pmap (fun (p : ) (pp : p.Prime) => ) b.factors ).prod
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 : ) :
= 1

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

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

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

theorem jacobiSym.legendreSym.to_jacobiSym (p : ) [fp : Fact p.Prime] (a : ) :
=

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 : ) :
= 0 = 1 = -1

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

@[simp]
theorem jacobiSym.one_left (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 : } [] :
= 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) :
0

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

theorem jacobiSym.eq_zero_iff {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) :
= 0

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

theorem jacobiSym.eq_one_or_neg_one {a : } {b : } (h : a.gcd b = 1) :
= 1 = -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 = ^ e

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

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

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

theorem jacobiSym.sq_one {a : } {b : } (h : a.gcd b = 1) :
^ 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) 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 p.Prime] {a : } (h : = -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 : } {n : } :
jacobiSym l.prod n = (List.map (fun (a : ) => ) 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 : } (hl : nl, n 0) :
jacobiSym a l.prod = (List.map (fun (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 : = -1) :
∃ (p : ), p.Prime p n = -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 : = -1) :

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

theorem ZMod.nonsquare_iff_jacobiSym_eq_neg_one {a : } {p : } [Fact p.Prime] :
= -1 ¬IsSquare a

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 p.Prime] (h : = 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} [] (χ : R →* ) (hp : ∀ (p : ) (pp : p.Prime), p 2 = χ p) {b : } (hb : Odd 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 *

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

theorem jacobiSym.at_two {b : } (hb : Odd 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 =
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) =

def qrSign (m : ) (n : ) :

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 % (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.