Commit 2024-03-20 19:03 4e3a4424
View on Github →feat(NumberTheory/LSeries/Deriv): derivatives of L-series (#11245)
This adds a file Mathlib.NumberTheory.LSeries.Deriv
that contains results on differentiability and derivatives of L-series, including the fact that the L-series is holomorphic on its right half-plane of absolute convergence.
See this thread on Zulip.