Theorem EisensteinSeries.abs_norm_eq_max_natAbs_neg

Modification history

2025-09-17 01:02
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
chore: tidy various files (#29635)
Modified EisensteinSeries.abs_norm_eq_max_natAbs_negView on Github →
2025-09-08 19:47
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
feat(Analysis/SpecialFunctions): iterated derivative of cotangent (#27212)
Added EisensteinSeries.abs_norm_eq_max_natAbs_negView on Github →