Commit 2024-05-17 09:11 21ec4834

feat(NumberTheory/EulerProduct/DirichletLSeries): use infinite product and L-series (#12809) This is a follow-up to [#12161](https://github.com/leanprover-community/mathlib4/pull/12161). It adds HasProd and tsum versions of the Euler Product statements for the Riemann zeta function and Dirichlet L-series (in the latter case, also replacing the explicit infinite sum by L ↗χ s). See this Zulip thread.