Theorems · Theorem · number theory

DirichletCharacter.LFunctionTrivChar_residue_one

∀ {N : ℕ} [inst : NeZero N],
  Filter.Tendsto (fun s => (s - 1) * DirichletCharacter.LFunctionTrivChar N s) (nhdsWithin 1 {1}ᶜ)
    (nhds (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

The L function of the trivial Dirichlet character mod N has a simple pole with residue ∏ p ∈ N.primeFactors, (1 - p⁻¹) at s = 1.

Defined in

Mathlib.NumberTheory.LSeries.DirichletContinuation

Cited by

2 results in Mathlib

Foundations

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

Assumes

NeZero