Theorem EisensteinSeries.r_mul_max_le
Modification history
2025-06-09 13:00
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
chore : Split summability results for Eisenstein series into own file (#25443) …
Modified EisensteinSeries.r_mul_max_leView on Github →