Theorems · Theorem · number theory

ZMod.completedLFunction_one_sub_even

∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Even Φ →
    ∀ (s : ℂ),
      s ≠ 0 ∨ ∑ j, Φ j = 0 →
        s ≠ 1 ∨ Φ 0 = 0 → ZMod.completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * ZMod.completedLFunction (ZMod.dft Φ) s

Functional equation for completed L-functions (even case), valid at all points of differentiability.

Defined in

Mathlib.NumberTheory.LSeries.ZMod

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZero