Theorems · Theorem · number theory

DirichletCharacter.LFunction_eq_completed_div_gammaFactor

∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ),
  s ≠ 0 ∨ N ≠ 1 → DirichletCharacter.LFunction χ s = DirichletCharacter.completedLFunction χ s / χ.gammaFactor s

Relation between the completed L-function and the usual one. We state it this way around so it holds at the poles of the gamma factor as well.

Defined in

Mathlib.NumberTheory.LSeries.DirichletContinuation

Cited by

0 results in Mathlib

Foundations

Depth 307 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NeZero