differentiable_completedZeta₀ — Mathlib

English

The modified completed zeta function Λ₀ is differentiable everywhere in ℂ.

Русский

Изменённая завершённая функция ζ ранее Λ₀ дифференцируема во всём комплексном плане.

LaTeX

$$$\\text{Differentiable } \\mathbb{C} \\; completedRiemannZeta_0$$$

Lean4

/-- The modified completed Riemann zeta function `Λ(s) + 1 / s + 1 / (1 - s)` is entire. -/
theorem differentiable_completedZeta₀ : Differentiable ℂ completedRiemannZeta₀ :=
  differentiable_completedHurwitzZetaEven₀ 0

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