Commit 2023-03-01 21:21 f06058e6

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.