Theorem EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq

Modification history

2026-01-28 16:26
Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Summable.lean
feat(NumberTheory/ModularForms/EisensteinSeries/E2/Transform): E2 under the action of SL2 (#32585) …
Added EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eqView on Github →