Def EisensteinSeries.eisSummand

Modification history

2024-07-09 17:23

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean

Chore: Rename files with Eisenstein series stuff. (#14572) …

Modified EisensteinSeries.eisSummand View on Github →

2024-07-08 13:05

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean

Eisenstein series are bounded at infinity (#12456) …

Modified EisensteinSeries.eisSummand View on Github →

2024-01-19 11:22

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean

feat: add definition of Eisenstein series (#9783) …

Added EisensteinSeries.eisSummand View on Github →