Theorem ModularGroup.SL_to_GL_tower

Modification history

2026-04-29 15:47
Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean
refactor(Analysis/Complex/UpperHalfPlane): deprecate old GL2Pos stuff (#38700) …
Added ModularGroup.SL_to_GL_towerView on Github →