Eisenstein series are modular forms

[CBirkbeck]

trafficstars

We show Eisenstein series are modular forms.

---

• [ ] depends on: #12456

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12456~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary 255342ca38

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.ModularForms.EisensteinSeries.ModularForm	1847

---

Declarations diff

+ _root_.eisensteinSeries + eisensteinSeries_MF - eisensteinSeries

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[mathlib-bors[bot]]

:v: CBirkbeck can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[CBirkbeck]

As for the TODO, I already have this, but its waiting on the q-expansion stuff thats coming. Should that still be a todo if its in the process of being PRd?

[grunweg]

As for the TODO, I already have this, but its waiting on the q-expansion stuff thats coming. Should that still be a todo if its in the process of being PRd?

I would do so - the next PR can remove the TODO. If that other PR doesn't land soon (for whatever reason), the current file is in a more useful state.

[CBirkbeck]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style