Commit 2023-12-06 14:30 561ab098

View on Github →

feat(NumberTheory/EulerProduct): add Euler Products for zeta function and Dirichlet L series (#8751) This adds proofs of the Euler product formula for the Riemann zeta function and Dirichlet L-series.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Complex/Abs.lean

added theorem Complex.ne_zero_of_one_lt_re

added theorem Complex.re_neg_ne_zero_of_one_lt_re

Created Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean

added theorem dirichletLSeries_eulerProduct

added def dirichletSummandHom

added def riemannZetaSummandHom

added theorem riemannZeta_eulerProduct

added theorem summable_dirichletSummand

added theorem summable_riemannZetaSummand