Theorems · Theorem · number theory

DirichletCharacter.LSeries_twist_vonMangoldt_eq

∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ},
  1 < s.re →
    LSeries ((fun n => χ ↑n) * fun n => ↑(ArithmeticFunction.vonMangoldt n)) s =
      -deriv (LSeries fun n => χ ↑n) s / LSeries (fun n => χ ↑n) s

The L-series of the twist of the von Mangoldt function Λ by a Dirichlet character χ at s equals the negative logarithmic derivative of the L-series of χ when re s > 1.

Defined in

Mathlib.NumberTheory.LSeries.Dirichlet

Cited by

2 results in Mathlib

Foundations

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