Kronecker symbol $\left(\frac{d}{m}\right)$ and fundamental discriminants

This file defines the two arithmetic notions used to state Dirichlet's class number formula.

1. Fundamental discriminant. An integer $d$ is a fundamental discriminant if $d \neq 1$ and either $d \equiv 1 \pmod 4$ and $d$ is squarefree, or $d = 4m$ with $m \equiv 2$ or $3 \pmod 4$ and $m$ squarefree. These are exactly the discriminants of quadratic number fields.

2. Kronecker symbol. For an integer $d$ and a natural number $m \ge 1$, write $m = 2^k m'$ with $m'$ odd. The Kronecker symbol is

where $\left(\frac{d}{m'}\right)$ is the Jacobi symbol and $\left(\frac{d}{2}\right)$ equals $0$ if $d$ is even, $1$ if $d \equiv \pm 1 \pmod 8$ and $-1$ if $d \equiv \pm 3 \pmod 8$. For $m = 0$ the value is $1$ if $d = \pm 1$ and $0$ otherwise.

For a fundamental discriminant $d$, the map $m \mapsto \left(\frac{d}{m}\right)$ is the real Dirichlet character $\chi$ modulo $|d|$ appearing in Dirichlet's class number formula.

Formalization Note kroneckerTwo d is Mathlib's character ZMod.χ₈ evaluated at $d \bmod 8$; the odd part uses Mathlib's jacobiSym. The value at $m = 0$ never enters an $L$-series.