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.

Estimated changes