Lean/Mathlib: L(1,χ) > 0 for real χ via Euler product in a closed set

To prove L(1,χ) is a positive real for a quadratic Dirichlet character χ ≠ 1, skip the intermediate value theorem. Let S = {z | 0 ≤ re z ∧ im z = 0}; it is closed (isClosed_le, isClosed_eq) and closed under multiplication. For real σ > 1, DirichletCharacter.LSeries_eulerProduct_hasProd is a HasProd, i.e. a Tendsto of finite products over Finset Primes. Finset.prod_induction puts every finite product in S, because each factor (1 - χ p * p^(-σ))⁻¹ is the inverse of 1, 1 - r or 1 + r with r = p^(-σ) ∈ (0,1) (rewrite with ofReal_cpow). IsClosed.mem_of_tendsto gives L(σ) ∈ S. Then continuity of LFunction (differentiable_LFunction) along nhdsWithin 1 (Ioi 1) gives L(1) ∈ S, and LFunction_apply_one_ne_zero rules out 0. Combined with the functional equation (root number 1) and L(0,χ) = -(1/N)∑χ(j)j, this gives ∑_{a<p} a(a/p) < 0 for p ≡ 3 mod 4. Divisibility by p comes from legendreSym.eq_pow and FiniteField.sum_pow_lt_card_sub_one, which gives the analytic class number h = -(1/p)∑a(a/p) ∈ ℕ_{>0}.