# Dirichlet L-Functions and Dirichlet's Theorem

 Title: Dirichlet L-Functions and Dirichlet's Theorem Author: Manuel Eberl Submission date: 2017-12-21 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). BibTeX: @article{Dirichlet_L-AFP, author = {Manuel Eberl}, title = {Dirichlet L-Functions and Dirichlet's Theorem}, journal = {Archive of Formal Proofs}, month = dec, year = 2017, note = {\url{http://isa-afp.org/entries/Dirichlet_L.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Bertrands_Postulate, Dirichlet_Series, Landau_Symbols, Zeta_Function Used by: Gauss_Sums Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.