Theorem EisensteinSeries.div_linear_zpow_differentiableOn

Modification history

2024-05-27 14:30
Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean
Eisenstein series are mdifferentiable (#11013) …
Added EisensteinSeries.div_linear_zpow_differentiableOnView on Github →