Theorem differentiableAt_expZeta

Modification history

2024-05-30 12:50

Mathlib/NumberTheory/LSeries/HurwitzZeta.lean

chore(NumberTheory/LSeries): namespace Hurwitz zeta (#13377) …

Deleted differentiableAt_expZeta View on Github →

2024-05-27 06:08

Mathlib/NumberTheory/LSeries/HurwitzZeta.lean

feat (NumberTheory/LSeries): Hurwitz zeta (#12897) …

Added differentiableAt_expZeta View on Github →