Commit 2021-12-04 05:05 9c4e41ae

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 𝒟.