Documentation

Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous

Arithmetic subgroups act properly discontinuously #

source
instance properlyDiscontinuousSL2ZRange :
ProperlyDiscontinuousSMul (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range) UpperHalfPlane
source
instance Subgroup.IsArithmetic.properlyDiscontinuous {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] :
ProperlyDiscontinuousSMul (↥𝒢) UpperHalfPlane

Arithmetic subgroups of GL(2, ℝ) act properly discontinuously on ℍ.