mathlib3

4e634b97 - feat(number_theory/modular_forms/slash_invariant_forms): define slash-invariant forms (#17677)

feat(number_theory/modular_forms/slash_invariant_forms): define slash-invariant forms (#17677) We define a new class of functions called `slash_invariant_forms` which will form the basis of the definition for modular forms. This is split from #13250 to make the PR smaller.