Theorems · Theorem · number theory

ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux

∀ {q : ℕ} (a : ZMod q) [inst : NeZero q],
  ContinuousOn (ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a) {s | 1 ≤ s.re}

The L-series of the von Mangoldt function restricted to the prime residue class a mod q is continuous on re s ≥ 1 except for a simple pole at s = 1 with residue (q.totient)⁻¹. The statement as given here in terms of ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux is equivalent.

Defined in

Mathlib.NumberTheory.LSeries.PrimesInAP

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZero