Theorems · Theorem · number theory

ZMod.differentiableAt_completedLFunction

∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) (s : ℂ),
  s ≠ 0 ∨ Φ 0 = 0 → s ≠ 1 ∨ ∑ j, Φ j = 0 → DifferentiableAt ℂ (ZMod.completedLFunction Φ) s

The completed L-function of a function ZMod N → ℂ is differentiable, with the following exceptions: at s = 1 if ∑ j, Φ j ≠ 0; and at s = 0 if Φ 0 ≠ 0.

Defined in

Mathlib.NumberTheory.LSeries.ZMod

Cited by

3 results in Mathlib

Foundations

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

Assumes

NeZero