differentiableAt_LFunction — Mathlib

English

The L-function of a Dirichlet character is differentiable everywhere except possibly at s = 1 in the trivial character case.

Русский

L-функция Dirichlet-перасонажа дифференцируема во всех точках кроме возможной точки s = 1 в случае тривиального символа.

LaTeX

$$differentiableAt_LFunction (χ) s =$$

Lean4

/-- The L-function of a Dirichlet character is differentiable, except at `s = 1` if the character is
trivial.
-/
@[fun_prop]
theorem differentiableAt_LFunction (χ : DirichletCharacter ℂ N) (s : ℂ) (hs : s ≠ 1 ∨ χ ≠ 1) :
    DifferentiableAt ℂ (LFunction χ) s :=
  ZMod.differentiableAt_LFunction χ s (hs.imp_right χ.sum_eq_zero_of_ne_one)

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