mathlib

f06058e6 - feat(analysis/complex/upper_half_plane/metric): prove that SL(2, ℝ) acts isometrically on upper half space with the hyperbolic metric (#18379)

feat(analysis/complex/upper_half_plane/metric): prove that SL(2, ℝ) acts isometrically on upper half space with the hyperbolic metric (#18379) A key part of the argument is to show that the element `modular_group.S` acts isometrically. We thus move the definition `modular_group.S` (and its partner `modular_group.T`) earlier in the import hierarchy to make it available without introducing a dependency on the theory of the modular group. Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: RuizheWan <115158055+RuizheWan@users.noreply.github.com>