Documentation
SpherePacking
.
ForMathlib
.
UpperHalfPlane
Search
return to top
source
Imports
Init
Mathlib.Data.Fintype.Parity
Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Imported by
ModularGroup
.
modular_S_sq
The Upper Half-Plane
#
Auxiliary lemmas about the upper half-plane.
source
theorem
ModularGroup
.
modular_S_sq
:
S
*
S
=
-
1