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