Theorems · Theorem · number theory

DirichletCharacter.eulerProduct_log_eq_LSeries

∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ},
  1 < s.re →
    ∑' (p : Nat.Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s)) =
      LSeries (fun n => χ ↑n * ↑(ArithmeticFunction.vonMangoldt n) / ↑(Real.log ↑n)) s

For 1 < s.re, the sum over primes of -log (1 - χ p * p ^ (-s)) — the logarithm of the Euler product — equals the L-series of n ↦ χ n * Λ n / Real.log n.

Defined in

Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Cited by

1 results in Mathlib

Foundations

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