EulerProducts

An attempt at formalizing facts on Euler products and L-series more generally in Lean

Most of the results developed here have by now made it into Mathlib, most notably a proof of Drichlet's Theorem on Primes in Residue Classes.

Apart from the uniqueness result for L-series, what is currently left in this repository are some bits and pieces that were not needed for the big result, but may still be useful.

Contents: