Kronecker symbol and quadratic characters

DefinitionFundamental discriminant#✓fully proved

An integer \(D\) is a fundamental discriminant if either \(D\) is squarefree and \(D \equiv 1 \pmod 4\), or \(D = 4m\) for some squarefree integer \(m\) with \(m \equiv 2 \pmod 4\) or \(m \equiv 3 \pmod 4\).

With this definition \(D = 1\) is a fundamental discriminant and \(D = 0\) is not.

public def IsFundamentalDiscriminant (D : ℤ) : Prop :=
  (Squarefree D ∧ D % 4 = 1) ∨
    ∃ m : ℤ, D = 4 * m ∧ Squarefree m ∧ (m % 4 = 2 ∨ m % 4 = 3)

Used by 6

Used byFundamental imaginary quadratic discriminant · Characterization of fundamental imaginary quadratic discriminants · Negative fundamental discriminants are fundamental imaginary quadratic discriminants · Fundamental imaginary quadratic discriminants are fundamental discriminants · Fundamental imaginary quadratic discriminants are imaginary quadratic discriminants · Quadratic Dirichlet character of a fundamental discriminant

DefinitionKronecker symbol at two#✓fully proved

For an integer \(D\), the Kronecker symbol of \(D\) at \(2\) is \(0\) if \(D\) is even, \(1\) if \(D \equiv \pm 1 \pmod 8\), and \(-1\) if \(D \equiv \pm 3 \pmod 8\).

public def kroneckerAtTwo (D : ℤ) : ℤ :=
  if D % 2 = 0 then 0
  else if D % 8 = 1 ∨ D % 8 = 7 then 1
  else -1

Used by 3

Used byKronecker symbol at a prime · Kronecker and Jacobi symbols agree at odd primes · Quadratic Dirichlet character of a fundamental discriminant

DefinitionKronecker symbol at a prime#✓fully proved

For an integer \(D\) and a natural number \(p\), the Kronecker symbol of \(D\) at \(p\) is the Kronecker symbol of \(D\) at two if \(p = 2\), the Legendre symbol \(\left(\frac{D}{p}\right)\) if \(p\) is an odd prime, and \(0\) if \(p\) is not prime.

public def kroneckerAtPrime (D : ℤ) (p : ℕ) : ℤ :=
  if p = 2 then kroneckerAtTwo D
  else if h : p.Prime then @legendreSym p (Fact.mk h) D
  else 0

Uses 1 · Used by 6

Statement usesKronecker symbol at two

Used byKronecker symbol at odd numbers for integers congruent to 3 mod 4 · Kronecker–Jacobi bridge for 4m with m ≡ 3 mod 4 · Kronecker symbol · Kronecker and Jacobi symbols agree at odd primes · Kronecker symbol with a prime denominator · Quadratic Dirichlet character of a fundamental discriminant

DefinitionKronecker symbol#✓fully proved

For an integer \(D\) and a natural number \(n\), the Kronecker symbol \(\left(\frac{D}{n}\right)\) is defined as follows. If \(n = 0\), it is \(1\) when \(D = \pm 1\) and \(0\) otherwise. If \(n \ge 1\) and \(n = p_1 p_2 \cdots p_k\) is the factorization of \(n\) into primes, listed with multiplicity, it is the product of the Kronecker symbols of \(D\) at the primes \(p_1, \ldots, p_k\) (the empty product \(1\) when \(n = 1\)).

public def kroneckerSym (D : ℤ) (n : ℕ) : ℤ :=
  if n = 0 then if D.natAbs = 1 then 1 else 0
  else (n.primeFactorsList.map (kroneckerAtPrime D)).prod

Uses 1 · Used by 8

Statement usesKronecker symbol at a prime

Used byKronecker symbol at odd numbers for integers congruent to 3 mod 4 · Quadratic reciprocity for the Kronecker symbol, positive \(D \equiv 1 \pmod 4\) · Kronecker symbol at odd primes for negative integers congruent to 1 mod 4 · Kronecker symbol at odd primes for integers congruent to 1 mod 4 · Kronecker–Jacobi bridge for 4m with m ≡ 3 mod 4 · Kronecker and Jacobi symbols agree at odd primes · Kronecker symbol with a prime denominator · Quadratic Dirichlet character of a fundamental discriminant

TheoremKronecker symbol with a prime denominator#✓fully proved

For every integer \(D\) and every prime \(p\), the Kronecker symbol \(\left(\frac{D}{p}\right)\) equals the Kronecker symbol of \(D\) at the prime \(p\).

public theorem kroneckerSym_prime (D : ℤ) (p : ℕ) (hp : p.Prime) :
    kroneckerSym D p = kroneckerAtPrime D p

Uses 2 · Used by 1

Statement usesKronecker symbol at a prime · Kronecker symbol

Used byKronecker and Jacobi symbols agree at odd primes

TheoremKronecker and Jacobi symbols agree at odd primes#✓fully proved

For every integer \(D\) and every prime \(p \ne 2\), the Kronecker symbol \(\left(\frac{D}{p}\right)\) equals the Jacobi symbol \(\left(\frac{D}{p}\right)\).

public theorem kroneckerSym_eq_jacobiSym_of_prime_ne_two (D : ℤ)
    (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) :
    kroneckerSym D p = jacobiSym D p

Uses 4 · Used by 5

Statement usesKronecker symbol

Proof usesKronecker symbol at a prime · Kronecker symbol at two · Kronecker symbol with a prime denominator

Used byKronecker symbol at odd numbers for integers congruent to 3 mod 4 · Quadratic reciprocity for the Kronecker symbol, positive \(D \equiv 1 \pmod 4\) · Kronecker symbol at odd primes for negative integers congruent to 1 mod 4 · Kronecker–Jacobi bridge for 4m with m ≡ 3 mod 4 · Quadratic Dirichlet character of a fundamental discriminant

TheoremQuadratic Dirichlet character of a fundamental discriminant#✓fully proved

Let \(D\) be a fundamental discriminant. Then there is a unique integer-valued Dirichlet character \(\chi\) modulo \(|D|\) such that \(\chi(n \bmod |D|) = \left(\frac{D}{n}\right)\) for every natural number \(n\), where \(\left(\frac{D}{n}\right)\) is the Kronecker symbol.

theorem quadraticDirichletCharacter (D : ℤ)
    (hD : IsFundamentalDiscriminant D) :
    ∃! χ : DirichletCharacter ℤ D.natAbs,
      ∀ n : ℕ, χ (n : ZMod D.natAbs) = kroneckerSym D n

Sources

• Joshua Males, Andreas Mono, Larry Rolen, and Ian Wagner, Central L-values of newforms and local polynomials, arXiv:2306.15519v5, subsection "L-functions and L-values", line 455. Exact source sentence: "One may also consider L-functions associated to a Dirichlet character chi_D = (D / dot), namely ...". This is the existence and uniqueness of the integer-valued Dirichlet character of level Int.natAbs D evaluating as the positive-denominator Kronecker symbol kroneckerSym D at every natural n, assuming IsFundamentalDiscriminant D. No primitivity or conductor claim belongs to this item.

Uses 5

Statement usesFundamental discriminant · Kronecker symbol

Proof usesKronecker symbol at a prime · Kronecker symbol at two · Kronecker and Jacobi symbols agree at odd primes

TheoremQuadratic reciprocity for the Kronecker symbol, positive \(D \equiv 1 \pmod 4\)#✓fully proved

Let \(D\) be a positive integer with \(D \equiv 1 \pmod 4\) and let \(p\) be an odd prime. Then the Jacobi symbol \(\left(\frac{p}{|D|}\right)\) equals the Kronecker symbol \(\left(\frac{D}{p}\right)\).

The congruence condition cannot be dropped: for \(D = 3\) and \(p = 7\) the Jacobi symbol \(\left(\frac{7}{3}\right)\) is \(1\), while the Kronecker symbol \(\left(\frac{3}{7}\right)\) is \(-1\).

public theorem jacobiSym_natAbs_eq_kroneckerSym_of_prime_ne_two_of_one_mod_four_pos
    (D : ℤ) (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (hpos : 0 < D)
    (h1 : D % 4 = 1) :
    jacobiSym (p : ℤ) D.natAbs = kroneckerSym D p

Uses 2 · Used by 1

Statement usesKronecker symbol

Proof usesKronecker and Jacobi symbols agree at odd primes

Used byKronecker symbol at odd primes for integers congruent to 1 mod 4

TheoremKronecker symbol at odd primes for negative integers congruent to 1 mod 4#✓fully proved

Let \(D\) be a negative integer with \(D \equiv 1 \pmod 4\) and let \(p\) be an odd prime. Then the Jacobi symbol \(\left(\frac{p}{|D|}\right)\) equals the Kronecker symbol \(\left(\frac{D}{p}\right)\).

public theorem jacobiSym_natAbs_eq_kroneckerSym_of_prime_ne_two_of_one_mod_four_neg
    (D : ℤ) (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (hneg : D < 0)
    (h1 : D % 4 = 1) :
    jacobiSym (p : ℤ) D.natAbs = kroneckerSym D p

Uses 2 · Used by 1

Statement usesKronecker symbol

Proof usesKronecker and Jacobi symbols agree at odd primes

Used byKronecker symbol at odd primes for integers congruent to 1 mod 4

TheoremKronecker symbol at odd primes for integers congruent to 1 mod 4#✓fully proved

Let \(D\) be an integer with \(D \equiv 1 \pmod 4\) and let \(p\) be an odd prime. Then the Jacobi symbol \(\left(\frac{p}{|D|}\right)\) equals the Kronecker symbol \(\left(\frac{D}{p}\right)\).

This covers \(D\) of either sign. The congruence condition cannot be dropped: for \(D = 3\) and \(p = 7\) the Jacobi symbol is \(1\) while the Kronecker symbol is \(-1\).

public theorem jacobiSym_natAbs_eq_kroneckerSym_of_prime_ne_two_of_one_mod_four
    (D : ℤ) (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (h1 : D % 4 = 1) :
    jacobiSym (p : ℤ) D.natAbs = kroneckerSym D p

Uses 3

Statement usesKronecker symbol

Proof usesKronecker symbol at odd primes for negative integers congruent to 1 mod 4 · Quadratic reciprocity for the Kronecker symbol, positive \(D \equiv 1 \pmod 4\)

TheoremKronecker symbol at odd numbers for integers congruent to 3 mod 4#✓fully proved

Let \(\chi_4\) be the nontrivial Dirichlet character modulo \(4\), so \(\chi_4(n) = 1\) for \(n \equiv 1 \pmod 4\) and \(\chi_4(n) = -1\) for \(n \equiv 3 \pmod 4\). Let \(D\) be an integer with \(D \equiv 3 \pmod 4\) and let \(p\) be an odd natural number. Then \(\chi_4(p) \cdot \left(\frac{p}{|D|}\right) = \left(\frac{D}{p}\right)\), where \(\left(\frac{p}{|D|}\right)\) is the Jacobi symbol and \(\left(\frac{D}{p}\right)\) is the Kronecker symbol.

For \(D > 0\) the factor \(\chi_4(p)\) is the sign from quadratic reciprocity; for \(D < 0\) it is the value \(\left(\frac{-1}{p}\right) = \chi_4(p)\).

public theorem chi4_mul_jacobiSym_natAbs_eq_kroneckerSym_of_odd_of_three_mod_four
    (D : ℤ) (p : ℕ) (hp_odd : Odd p) (h3 : D % 4 = 3) :
    (ZMod.χ₄ p : ℤ) * jacobiSym (p : ℤ) D.natAbs = kroneckerSym D p

Uses 3 · Used by 1

Statement usesKronecker symbol

Proof usesKronecker symbol at a prime · Kronecker and Jacobi symbols agree at odd primes

Used byKronecker–Jacobi bridge for 4m with m ≡ 3 mod 4

TheoremJacobi symbol of \(4m\) at an odd denominator#✓fully proved

For every integer \(m\) and every odd natural number \(p\), the Jacobi symbol \(\left(\frac{4m}{p}\right)\) equals \(\left(\frac{m}{p}\right)\).

public theorem jacobiSym_four_mul_of_odd (m : ℤ) (p : ℕ) (hp_odd : Odd p) :
    jacobiSym (4 * m) p = jacobiSym m p

Used by 1

Used byKronecker–Jacobi bridge for 4m with m ≡ 3 mod 4

TheoremJacobi symbol of \(2m\) at an odd denominator#✓fully proved

For every integer \(m\) and every odd natural number \(p\), the Jacobi symbol \(\left(\frac{2m}{p}\right)\) equals \(\chi_8(p) \left(\frac{m}{p}\right)\), where \(\chi_8\) is the Dirichlet character modulo \(8\) with \(\chi_8(n) = 1\) for \(n \equiv \pm 1 \pmod 8\), \(\chi_8(n) = -1\) for \(n \equiv \pm 3 \pmod 8\), and \(\chi_8(n) = 0\) for even \(n\).

public theorem jacobiSym_two_mul_of_odd (m : ℤ) (p : ℕ) (hp_odd : Odd p) :
    jacobiSym (2 * m) p = (ZMod.χ₈ p : ℤ) * jacobiSym m p

TheoremKronecker–Jacobi bridge for 4m with m ≡ 3 mod 4#✓fully proved

Even m % 4 = 3 subcase for odd p: reduce 4 * m to m, identify kroneckerSym with jacobiSym at odd denominators, then apply the D % 4 = 3 bridge to m itself. Covers prime and composite odd denominators alike.

public theorem
    chi4_mul_jacobiSym_natAbs_eq_kroneckerSym_of_odd_of_four_mul_three_mod_four
    (m : ℤ) (p : ℕ) (hp_odd : Odd p) (h3 : m % 4 = 3) :
    (ZMod.χ₄ p : ℤ) * jacobiSym (p : ℤ) m.natAbs = kroneckerSym (4 * m) p

Uses 5

Statement usesKronecker symbol

Proof usesKronecker symbol at odd numbers for integers congruent to 3 mod 4 · Jacobi symbol of \(4m\) at an odd denominator · Kronecker symbol at a prime · Kronecker and Jacobi symbols agree at odd primes

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.