Commit 2024-02-15 22:29 25577a7e

refactor : add namespace UpperHalfPlane.ModularGroup (#7885) Rename some definitions and theorems about $SL(2, ℤ)$ in Analysis/Complex/UpperHalfPlane/Basic.lean to place them in the namespace UpperHalfPlane.ModularGroup, in order to avoid the confusion with definitions and theorems about $SL(2, ℝ)$. For example, UpperHalfPlane.det_coe' is renamed to UpperHalfPlane.ModularGroup.det_coe', because we will have UpperHalfPlane.SL2R.det_coe'.