Theorem LSeriesHasSum_cos

Modification history

2024-05-30 12:50

Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean

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

Deleted LSeriesHasSum_cos View on Github →

2024-05-06 07:35

Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean

feat(NumberTheory/LSeries): Even Hurwitz zeta functions (II) (#12265) …

Added LSeriesHasSum_cos View on Github →