abscissaOfAbsConv_zeta — Mathlib

English

The abscissa of absolute convergence of the arithmetic function ζ is 1.

Русский

Абсцисса абсолютной конвергенции арифметической функции ζ равна 1.

LaTeX

$$$\operatorname{abscissaOfAbsConv}(\uparrow ζ) = 1.$$$

Lean4

/-- The abscissa of (absolute) convergence of the arithmetic function `ζ` is `1`. -/
theorem abscissaOfAbsConv_zeta : abscissaOfAbsConv ↗ζ = 1 := by
  rw [abscissaOfAbsConv_congr (g := 1) fun hn ↦ by simp [hn], abscissaOfAbsConv_one]

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