Structures · Algebra
Subgroup.IsArithmetic
A subgroup of GL(2, ℝ) is arithmetic if it is commensurable with the image of SL(2, ℤ).
- Shape
- One type argument · adds is_commensurable
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- MonoidHom.range
- Subgroup.adjoinNegOne
- Subgroup.map
- Min.min
How is a type an instance?
Loading the hierarchy index…
Assumed by52
- ModularForm.weakFEPair
- ModularForm.Λ
- Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z
- ModularForm.L
- cosetToCuspOrbit
- Subgroup.IsArithmetic.is_commensurable
- CuspForm.isStrongFEPair
- CuspFormClass.petersson_bounded_left
- ModularGroup.exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO
- qExpansion_coeff_isBigO_of_norm_isBigO
- ModularForm.weakFEPair_f
- CuspForm.hasSum_Λ
- ModularFormClass.bdd_at_infty_slash
- ModularForm.hasSum_Λ
- ModularFormClass.exists_bound
- ModularGroup.exists_bound_of_subgroup_invariant
- ModularFormClass.qExpansion_isBigO
- ModularFormClass.exists_petersson_le
- ModularForm.weakFEPair_f₀
- CuspForm.Λ_eq_mellin
- Subgroup.IsArithmetic.conj
- CuspForm.differentiable_Λ
- Subgroup.strictWidthInfty_pos
- CuspFormClass.exists_bound
- CuspFormClass.qExpansion_isBigO
- cosetToCuspOrbit.congr_simp
- instFactIsCuspInftyRealOfIsArithmetic
- ModularForm.weakFEPair_k
- ModularForm.eq_const_of_weight_zero
- Subgroup.IsArithmetic.inter
- ModularForm.weakFEPair.congr_simp
- ModularForm.weakFEPair_ε
- CuspForm.hasSum_L
- Subgroup.IsArithmetic.finiteIndex_comap
- Subgroup.IsArithmetic.isFiniteRelIndexSL
- CuspFormClass.petersson_bounded_right
- ModularForm.isZero_of_neg_weight
- cosetToCuspOrbit_apply_mk
- instFiniteCuspOrbitsOfIsArithmetic
- CuspForm.differentiable_L
- ModularForm.weakFEPair_g₀
- Subgroup.instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic
- Subgroup.IsArithmetic.discreteTopology
- CuspFormClass.zero_at_infty_slash
- ModularForm.Λ.congr_simp
- ModularForm.L.congr_simp
- Subgroup.IsArithmetic.properlyDiscontinuous
- Subgroup.widthInfty_pos
- ModularForm.hasSum_L
- surjective_cosetToCuspOrbit
Ancestors0
No ancestors.