Commit 2024-05-31 14:33 d0f61917

feat(NumberTheory/LSeries): Riemann zeta as special case of Hurwitz (#13273) We now have a general treatment of the Hurwitz zeta function. The Riemann zeta is just the Hurwitz zeta for a = 0, and this PR reimplements it as such. I have tried to carry over the align statements from the old treatment wherever possible (many of the intermediate lemmas from the previous iteration don't have direct analogues, but the main results do).