Theorems · Theorem · number theory

ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq

∀ {q : ℕ} {a : ZMod q} [inst : NeZero q],
  IsUnit a →
    ∀ {s : ℂ},
      1 < s.re →
        LSeries (fun n => ↑(ArithmeticFunction.vonMangoldt.residueClass a n)) s =
          -(↑q.totient)⁻¹ * ∑ χ, χ a⁻¹ * (deriv (DirichletCharacter.LFunction χ) s / DirichletCharacter.LFunction χ s)

The L-series of the von Mangoldt function restricted to the residue class a mod q with a invertible in ZMod q is a linear combination of logarithmic derivatives of L-functions of the Dirichlet characters mod q (on re s > 1).

Defined in

Mathlib.NumberTheory.LSeries.PrimesInAP

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZero