mathlib3

9c4e41ae - feat(number_theory/modular): the action of `SL(2, ℤ)` on the upper half plane (#8611)

feat(number_theory/modular): the action of `SL(2, ℤ)` on the upper half plane (#8611) We define the action of `SL(2,ℤ)` on `ℍ` (via restriction of the `SL(2,ℝ)` action in `analysis.complex.upper_half_plane`). We then define the standard fundamental domain `𝒟` for this action and show that any point in `ℍ` can be moved inside `𝒟`. Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Marc Masdeu <marc.masdeu@gmail.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Marc Masdeu <marc.masdeu@gmail.com>