Theorems · Theorem · number theory

ZMod.LFunction_eq_completed_div_gammaFactor_even

∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Even Φ → ∀ (s : ℂ), s ≠ 0 ∨ Φ 0 = 0 → ZMod.LFunction Φ s = ZMod.completedLFunction Φ s / s.Gammaℝ

Relation between the completed L-function and the usual one (even case). We state it this way around so it holds at the poles of the gamma factor as well (except at s = 0, where it is genuinely false if N > 1 and Φ 0 ≠ 0).

Defined in

Mathlib.NumberTheory.LSeries.ZMod

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZero