LFunction_ne_zero_of_one_le_re — Mathlib

English

For a Dirichlet character χ with NeZero N, and any s with Re s ≥ 1, if χ ≠ 1 or s ≠ 1, then LFunction χ(s) ≠ 0.

Русский

Для χ с NeZero N и любого s с Re s ≥ 1, если χ ≠ 1 или s ≠ 1, тогда LFunction χ(s) ≠ 0.

LaTeX

$$$\mathrm{Re}(s) \ge 1 \implies LFunction(χ,s) \neq 0 \quad(χ\neq 1 \lor s\neq 1).$$$

Lean4

/-- If `χ` is a Dirichlet character, then `L(χ, s)` does not vanish for `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_one_le_re ⦃s : ℂ⦄ (hχs : χ ≠ 1 ∨ s ≠ 1) (hs : 1 ≤ s.re) : LFunction χ s ≠ 0 :=
  hs.eq_or_lt.casesOn (fun hs ↦ LFunction_ne_zero_of_re_eq_one χ hs.symm hχs) fun hs ↦
    LFunction_eq_LSeries χ hs ▸ LSeries_ne_zero_of_one_lt_re χ hs

Похожие утверждения