Theorems · Theorem · number theory

DirichletCharacter.LSeries_changeLevel

∀ {M N : ℕ} [NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ},
  1 < s.re →
    LSeries (fun n => ((DirichletCharacter.changeLevel hMN) χ) ↑n) s =
      LSeries (fun n => χ ↑n) s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

If χ is a Dirichlet character and its level M divides N, then we obtain the L-series of χ considered as a Dirichlet character of level N from the L-series of χ by multiplying with ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s)).

Defined in

Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Cited by

0 results in Mathlib

Foundations

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

Assumes

NeZero