[Merged by Bors] - feat(NumberTheory/ModularForms/EisensteinSeries/Summable): add auxiliary E2 lemmas

[CBirkbeck]

This contains a series of lemmas that are needed in #32585 to prove how E2 transforms under the slash action.

---

[CBirkbeck]

Note I renamed a file (fixing a typo in the name) so the file was not actually removed.

[loefflerd]

The thing to do with the removed file is to not completely delete the old file, but move its contents elsewhere and keep the old file containing nothing but a deprecation warning, like this:

module

public import Name.Of.The.New.File

deprecated_module (since := "2025-12-19")

See Mathlib.Topology.PartialHomeomorph for an example. Then it will get autodeleted after 6 months. (I agree this is a bit overkill for this example, but the CI scripts will complain otherwise.)

[loefflerd]

I think this looks good now.

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by loefflerd.

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ 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.

[loefflerd]

This was failing CI due to some glitch in the testing system, unrelated to the PR. I just re-ran the failing test and it works fine now.

[CBirkbeck]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step