Theorems · Theorem · number theory

ZMod.LFunction_eq_completed_div_gammaFactor_odd

∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Odd Φ → ∀ (s : ℂ), ZMod.LFunction Φ s = ZMod.completedLFunction Φ s / (s + 1).Gammaℝ

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

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