Theorem Summable.tendsto_zero_of_even_summable_symmetricIcc

Modification history

2025-12-15 10:15
Mathlib/Topology/Algebra/InfiniteSum/ConditionalInt.lean
feat(NumberTheory/EisensteinSeries/E2): Define the Eisenstein series E2 (#32584) …
Added Summable.tendsto_zero_of_even_summable_symmetricIccView on Github →