Theorem EisensteinSeries.eisensteinSeries_SIF_MDifferentiable

Modification history

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