completedLFunction — Mathlib

English

The completed L-function is almost everywhere equal to the product L(χ, s) · gammaFactor(χ, s).

Русский

Завершённая L-функция равна почти везде произведению L(χ, s) и gammaFactor(χ, s).

LaTeX

$$$\text{completedLFunction}(\chi,s) = L(\chi,s) \cdot \gamma\text{Factor}(\chi,s)\quad\text{(almost everywhere)}$$$

Lean4

/-- The completed L-function of a Dirichlet character, almost everywhere equal to
`LFunction χ s * gammaFactor χ s`.
-/
@[pp_nodot]
noncomputable def completedLFunction (χ : DirichletCharacter ℂ N) (s : ℂ) : ℂ :=
  ZMod.completedLFunction χ s

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