English
If χ is a Dirichlet character and s lies on the line Re s = 1 with χ ≠ 1 or s ≠ 1, then LFunction χ(s) ≠ 0.
Русский
Если χ — символ Дирихле и s лежит на прямой Re s = 1 при χ ≠ 1 или s ≠ 1, то LFunction χ(s) ≠ 0.
LaTeX
$$$LFunction\left(\chi, s\right) \neq 0 \quad \text{whenever } \mathrm{Re}(s)=1 \text{ and } (χ\neq 1 \lor s\neq 1).$$$
Lean4
/-- If `χ` is a Dirichlet character, then `L(χ, s)` does not vanish when `s.re = 1`
except when `χ` is trivial and `s = 1` (then `L(χ, s)` has a simple pole at `s = 1`). -/
theorem LFunction_ne_zero_of_re_eq_one {s : ℂ} (hs : s.re = 1) (hχs : χ ≠ 1 ∨ s ≠ 1) : LFunction χ s ≠ 0 :=
by
by_cases h : χ ^ 2 = 1 ∧ s = 1
· exact h.2 ▸ LFunction_apply_one_ne_zero_of_quadratic h.1 <| hχs.neg_resolve_right h.2
· have hs' : s = 1 + I * s.im := by conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]
rw [not_and_or, ← ne_eq, ← ne_eq, hs', add_ne_left] at h
replace h : χ ^ 2 ≠ 1 ∨ s.im ≠ 0 := h.imp_right (fun H ↦ by exact_mod_cast right_ne_zero_of_mul H)
exact hs'.symm ▸ χ.LFunction_ne_zero_of_not_quadratic_or_ne_one h
