$L(1,\chi) > 0$ for a real non-principal character

Positivity of $L(1,\chi)$ for real characters. Let $\chi$ be a real (quadratic) non-principal Dirichlet character modulo $q \ge 1$. Then

Indeed $L(1,\chi)$ is real, it is nonzero (Dirichlet; Mathlib's DirichletCharacter.LFunction_apply_one_ne_zero), and it is the limit as $\sigma \to 1^+$ of $L(\sigma,\chi)$, which is positive for $\sigma > 1$ because $\zeta(\sigma)L(\sigma,\chi) = \sum_n \bigl(\sum_{d\mid n}\chi(d)\bigr)n^{-\sigma}$ has nonnegative coefficients and $\zeta(\sigma) > 0$. Siegel's theorem $L(1,\chi) > C(\varepsilon)q^{-\varepsilon}$ is a quantitative form of this positivity; the positivity itself is needed to pass from a lower bound for the product $L(1,\chi_1)L(1,\chi_2)L(1,\chi_1\chi_2)$ to one for a single factor.

Formalization Note. The statement asserts positivity of the real part; reality of $L(1,\chi)$ is the companion statement Davenport.LFunction_ofReal_im_eq_zero.