Def ModularForm.eisensteinSeriesMF

Modification history

2026-02-11 09:57

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean

chore: fix some names around Eisenstein series (#35055) …

Added ModularForm.eisensteinSeriesMF View on Github →