Theorems · Theorem · number theory

ZMod.LFunction_one_sub

∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) {s : ℂ},
  (∀ (n : ℕ), s ≠ -↑n) →
    Φ 0 = 0 ∨ s ≠ 1 →
      ZMod.LFunction Φ (1 - s) =
        ↑N ^ (s - 1) * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s *
          (Complex.exp (↑Real.pi * Complex.I * s / 2) * ZMod.LFunction (ZMod.dft Φ) s +
            Complex.exp (-↑Real.pi * Complex.I * s / 2) * ZMod.LFunction (ZMod.dft fun x => Φ (-x)) s)

Functional equation for ZMod L-functions, in terms of discrete Fourier transform.

Defined in

Mathlib.NumberTheory.LSeries.ZMod

Cited by

0 results in Mathlib

Foundations

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

Assumes

NeZero