modular_forms): reduce dependency on manifolds (#19212)

Commit

2 years ago

chore(analysis/complex/upper_half_plane,number_theory/modular_forms): reduce dependency on manifolds (#19212) Move some lemmas that use `mfderiv` or `mdifferentiable` to new files.

Author

urkud

Parents

d30d3126

mathlib 57f9349f - chore(analysis/complex/upper_half_plane,number_theory/modular_forms): reduce dependency on manifolds (#19212)

mathlib
57f9349f - chore(analysis/complex/upper_half_plane,number_theory/modular_forms): reduce dependency on manifolds (#19212)