Theorems · Theorem · number theory

ZMod.LFunction_stdAddChar_eq_expZeta

∀ {N : ℕ} [inst : NeZero N] (j : ZMod N) (s : ℂ),
  j ≠ 0 ∨ s ≠ 1 → ZMod.LFunction (fun k => ZMod.stdAddChar (j * k)) s = HurwitzZeta.expZeta (ZMod.toAddCircle j) s

The LFunction of the function x ↦ e (j * x), where e : ZMod N → ℂ is the standard additive character, is expZeta (j / N). Note this is not at all obvious from the definitions, and we prove it by analytic continuation from the convergence range.

Defined in

Mathlib.NumberTheory.LSeries.ZMod

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZero