Theorem EisensteinSeries.eisSummand_extension_differentiableOn

Modification history

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