Zero count for Dirichlet $L$-functions: $N(T,\chi)=\frac{T}{\pi}\log\frac{qT}{2\pi e}+O(\log qT)$

For a positive integer $q$ and a Dirichlet character $\chi$ modulo $q$, write $N(T,\chi)$ for the number of zeros $\rho$ of the Dirichlet $L$-function $L(s,\chi)$ with $0<\operatorname{Re}\rho<1$ and $-T\le\operatorname{Im}\rho\le T$, counted with multiplicity.

There is an absolute constant $C$ such that for every $q\ge1$, every primitive Dirichlet character $\chi$ modulo $q$ and every $T\ge2$,

In the usual notation, $N(T,\chi)=\frac{T}{\pi}\log\frac{qT}{2\pi e}+O(\log qT)$, uniformly in $q$ and $\chi$.

This is the analogue of the Riemann–von Mangoldt formula for Dirichlet $L$-functions; for $q=1$ (where $L(s,\chi)=\zeta(s)$ and $N(T,\chi)=2N(T)$) it recovers the formula for $\zeta$.

Formalization Note The source gives no range for $T$ and leaves the uniformity implicit; the draft uses the standard form (Davenport, Multiplicative Number Theory, Ch. 16): $T\ge2$, with one constant $C$ for all $q$ and all primitive $\chi$. $L(s,\chi)$ is Mathlib's DirichletCharacter.LFunction, primitivity is DirichletCharacter.IsPrimitive, and $N(T,\chi)$ is dirichletZeroCount χ T.