Theorems · Definition · number theory

ZMod.LFunction

{N : ℕ} → [NeZero N] → (ZMod N → ℂ) → ℂ → ℂ

The unique meromorphic function ℂ → ℂ which agrees with ∑' n : ℕ, Φ n / n ^ s wherever the latter is convergent. This is constructed as a linear combination of Hurwitz zeta functions. Note that this is not the same as LSeries Φ: they agree in the convergence range, but LSeries Φ s is defined to be 0 if re s ≤ 1.

Defined in

Mathlib.NumberTheory.LSeries.ZMod

Cited by

16 results in Mathlib

Foundations

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

Assumes

NeZero