Theorem EisensteinSeries.summable_linear_right_add_one_mul_linear_right

Modification history

2025-12-27 18:03

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean

feat(NumberTheory/ModularForms/EisensteinSeries/Summable): add auxiliary E2 lemmas (#32955) …

Added EisensteinSeries.summable_linear_right_add_one_mul_linear_right View on Github →