LFunction_apply_one_ne_zero — Mathlib

English

A variant of the previous nonvanishing result: on the half-plane Re s ≥ 1, unless χ^2 = 1 and s = 1, L(χ, s) ≠ 0.

Русский

Вариант предыдущего не нуль-результата: на пол-плоскости Re s ≥ 1 при χ^2 ≠ 1 или s ≠ 1 выполняется L(χ, s) ≠ 0.

LaTeX

$$$\text{If } χ^2 \neq 1 \text{ or } s \neq 1, \ then\ L(χ,s) \neq 0 \text{ for } \Re(s) \ge 1.$$$

Lean4

/-- The L-function of a nontrivial Dirichlet character does not vanish at `s = 1`. -/
theorem LFunction_apply_one_ne_zero (hχ : χ ≠ 1) : LFunction χ 1 ≠ 0 :=
  LFunction_ne_zero_of_one_le_re χ (.inl hχ) <| one_re ▸ le_rfl

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