feat(number_theory/modular): fundamental domain part 2 (#8985)
This completes the argument that the standard open domain `{z : |z|>1, |\Re(z)|<1/2}` is a fundamental domain for the action of `SL(2,\Z)` on `\H`. The first PR (#8611) showed that every point in the upper half plane has a representative inside its closure, and here we show that representatives in the open domain are unique.
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>
