Dirichlet L-Functions and Dirichlet's Theorem

Manuel Eberl 🌐

December 21, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This article provides a formalisation of Dirichlet characters and Dirichlet L-functions including proofs of their basic properties – most notably their analyticity, their areas of convergence, and their non-vanishing for ℜ(s) ≥ 1. All of this is built in a very high-level style using Dirichlet series. The proof of the non-vanishing follows a very short and elegant proof by Newman, which we attempt to reproduce faithfully in a similar level of abstraction in Isabelle.

This also leads to a relatively short proof of Dirichlet’s Theorem, which states that, if h and n are coprime, there are infinitely many primes p with ph (mod n).

BSD License


Theories of Dirichlet_L