completedLFunction_modOne_eq — Mathlib

English

For the unique Dirichlet character modulo 1, the completed L-function equals the completed Riemann zeta function.

Русский

Для единственного символа по модулю 1 совпадает завершённая L-функция с завершённой функцией Римана zeta.

LaTeX

$$$\text{completedLFunction}(\chi,s) = \text{completedRiemannZeta}(s)\quad\text{when } N=1$$$

Lean4

/-- The completed L-function of the (unique) Dirichlet character mod 1 is the completed Riemann zeta
function.
-/
theorem completedLFunction_modOne_eq {χ : DirichletCharacter ℂ 1} : completedLFunction χ = completedRiemannZeta := by
  ext; rw [completedLFunction, ZMod.completedLFunction_modOne_eq, map_one, one_mul]

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