LSeries_zeta_eq — Mathlib

English

The L-series of the arithmetic function ζ equals the L-series of the constant-1 sequence.

Русский

L-ряд арифметической функции ζ совпадает с L-рядом константы 1.

LaTeX

$$$L(\uparrow ζ) = L(1).$$$

Lean4

/-- The `LSeries` of the arithmetic function `ζ` is the same as the `LSeries` associated
to the constant sequence `1`. -/
theorem LSeries_zeta_eq : L ↗ζ = L 1 := by
  ext s
  exact (LSeries_congr const_one_eq_zeta s).symm

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