Theorems · Theorem · number theory

ZMod.LFunction_dft

∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) {s : ℂ},
  Φ 0 = 0 ∨ s ≠ 1 → ZMod.LFunction (ZMod.dft Φ) s = ∑ j, Φ j * HurwitzZeta.expZeta (ZMod.toAddCircle (-j)) s

Explicit formula for the L-function of 𝓕 Φ, where 𝓕 is the discrete Fourier transform.

Defined in

Mathlib.NumberTheory.LSeries.ZMod

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZero