theorem mainTheorem_quadratic {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) (χ_ne : χ ≠ 1) : χ.LFunction 1 ≠ 0

If χ is a nontrivial quadratic Dirichlet character, then L(χ, 1) ≠ 0.

theorem ourMainTheorem {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (t : ℝ) (hχt : χ ≠ 1 ∨ t ≠ 0) : χ.LFunction (1 + Complex.I * ↑t) ≠ 0

If χ is a Dirichlet character, then L(χ, 1 + I*t) does not vanish for t ∈ ℝ except when χ is trivial and t = 0 (then L(χ, s) has a simple pole at s = 1).