### Abstract

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
*p* ≡ *h* (mod
*n*).