Modular form finite-dimensionality

Stream: mathlib4

[David Loeffler]

In the light of Kevin's recent BdR post, which emphasised that finite-dimensionality of modular forms spaces is not yet in Mathlib, I'm happy to announce PR #32460, which proves the following step towards this: for any finite-index subgroup of SL(2, Z), there are no non-zero modular forms of negative weight. This is the base case for an inductive argument towards proving finite-dimensionality in all weights.