Documentation
LeanPool
.
LeanModularForms
.
ForMathlib
.
UpperHalfPlane
Search
return to top
source
Imports
Init
Mathlib.Data.Fintype.Parity
Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Imported by
ModularGroup
.
modular_S_sq
UpperHalfPlane
#
source
theorem
ModularGroup
.
modular_S_sq
:
S
*
S
=
-
1