Theorems · Theorem · number theory

DirichletCharacter.LSeries_eq_exp_LSeries

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

For 1 < s.re, the Dirichlet L-function is the exponential of the L-series of n ↦ χ n * Λ n / Real.log n.

Defined in

Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Cited by

1 results in Mathlib

Foundations

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