Cusps

📁 Source: Mathlib/NumberTheory/ModularForms/Cusps.lean

Statistics

Metric	Count
Definitions CuspOrbits, IsCusp, IsRegularAtInfty, periods, strictPeriods, strictWidthInfty, widthInfty, cosetToCuspOrbit, cusps_subMulAction	9
Theorems isCusp_iff, strictPeriods_Gamma, strictPeriods_Gamma0, strictPeriods_Gamma1, strictWidthInfty_Gamma, strictWidthInfty_Gamma0, strictWidthInfty_Gamma1, mono, of_isFiniteRelIndex, of_isFiniteRelIndex_conj, smul, smul_of_mem, exists_mem_SL2, isCusp_iff, isParabolic_iff_of_upperTriangular, isCusp_iff_isCusp_SL2Z, eq, commensurable_strictPeriods_periods, instDiscreteTopPeriods, instDiscreteTopStrictPeriods, isCusp_of_mem_strictPeriods, isRegularAtInfty_iff, isRegularAtInfty_of_neg_one_mem, mem_strictPeriods_iff, periods_eq_zmultiples_widthInfty, relIndex_strictPeriods, strictPeriods_SL2Z, strictPeriods_eq_periods_of_neg_one_mem, strictPeriods_eq_zmultiples_one_of_T_mem, strictPeriods_eq_zmultiples_strictWidthInfty, strictPeriods_le_periods, strictWidthInfty_SL2Z, strictWidthInfty_eq_one_of_T_mem, strictWidthInfty_mem_strictPeriods, strictWidthInfty_nonneg, strictWidthInfty_pos, strictWidthInfty_pos_iff, two_mul_withInfty_mem_strictPeriods, widthInfty_mem_periods, widthInfty_nonneg, widthInfty_pos, widthInfty_pos_iff, cosetToCuspOrbit_apply_mk, instFiniteCuspOrbitsOfIsArithmetic, isCusp_SL2Z_iff, isCusp_SL2Z_iff', isCusp_iff_of_relIndex_ne_zero, isCusp_iff_of_relindex_ne_zero, surjective_cosetToCuspOrbit	49
Total	58

Commensurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCusp_iff 📖	mathematical	Subgroup.Commensurable Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring	IsCusp	—	Subgroup.Commensurable.isCusp_iff

CongruenceSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictPeriods_Gamma 📖	mathematical	—	Subgroup.strictPeriods Real Real.instRing Subgroup.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Gamma AddSubgroup.zmultiples AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instNatCast	—	AddSubgroup.ext AddMonoidHom.map_zmultiples Int.cast_natCast Matrix.cons_val' Matrix.cons_val_fin_one AddSubgroup.mem_map_of_mem Int.mem_zmultiples_iff ZMod.intCast_zmod_eq_zero_iff_dvd ModularGroup.coe_T_zpow Int.cast_one Int.cast_mul CharP.cast_eq_zero ZMod.charP MulZeroClass.mul_zero Int.cast_zero Matrix.ext Fintype.complete
strictPeriods_Gamma0 📖	mathematical	—	Subgroup.strictPeriods Real Real.instRing Subgroup.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Gamma0 AddSubgroup.zmultiples AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instOne	—	Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem Matrix.cons_val' Matrix.cons_val_fin_one Int.cast_zero
strictPeriods_Gamma1 📖	mathematical	—	Subgroup.strictPeriods Real Real.instRing Subgroup.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Gamma1 AddSubgroup.zmultiples AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instOne	—	Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem Matrix.cons_val' Matrix.cons_val_fin_one Int.cast_one Int.cast_zero
strictWidthInfty_Gamma 📖	mathematical	—	Subgroup.strictWidthInfty Subgroup.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing Gamma Real.instNatCast	—	strictPeriods_Gamma AddSubgroup.zmultiples_eq_zmultiples_iff not_isOfFinAddOrder_of_isAddTorsionFree instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add NeZero.charZero RCLike.charZero_rclike Subgroup.strictPeriods_eq_zmultiples_strictWidthInfty Subgroup.instDiscreteTopStrictPeriods instIsTopologicalRingReal Subgroup.IsArithmetic.discreteTopology Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex instFiniteIndexGamma
strictWidthInfty_Gamma0 📖	mathematical	—	Subgroup.strictWidthInfty Subgroup.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing Gamma0 Real.instOne	—	Subgroup.strictWidthInfty_eq_one_of_T_mem Matrix.cons_val' Matrix.cons_val_fin_one Int.cast_zero
strictWidthInfty_Gamma1 📖	mathematical	—	Subgroup.strictWidthInfty Subgroup.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing Gamma1 Real.instOne	—	Subgroup.strictWidthInfty_eq_one_of_T_mem Matrix.cons_val' Matrix.cons_val_fin_one Int.cast_one Int.cast_zero

IsCusp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	Subgroup Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder IsCusp	—	—	—
of_isFiniteRelIndex 📖	—	IsCusp	—	—	Subgroup.relIndex_ne_zero mono inf_le_left isCusp_iff_of_relIndex_ne_zero inf_le_right Subgroup.inf_relIndex_right
of_isFiniteRelIndex_conj 📖	mathematical	IsCusp Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike	ConjAct SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Units.instDivInvMonoid MulAction.toSemigroupAction Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct	—	Subgroup.conjAct_pointwise_smul_eq_self Subgroup.le_normalizer Subgroup.relIndex_pointwise_smul Subgroup.relIndex_ne_zero of_isFiniteRelIndex
smul 📖	mathematical	IsCusp	Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction OnePoint.instGLAction Real.instField Real.decidableEq ConjAct Subgroup Units.instGroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Units.instDivInvMonoid Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct	—	Subgroup.smul_mem_pointwise_smul SemigroupAction.mul_smul inv_smul_smul
smul_of_mem 📖	mathematical	IsCusp Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike	OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid MulAction.toSemigroupAction OnePoint.instGLAction Real.instField Real.decidableEq	—	Subgroup.ext Subgroup.mem_pointwise_smul_iff_inv_smul_mem ConjAct.toConjAct_inv ConjAct.toConjAct_smul inv_inv Subgroup.mul_mem_cancel_right Subgroup.mul_mem_cancel_left InvMemClass.inv_mem SubgroupClass.toInvMemClass Subgroup.instSubgroupClass smul

OnePoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mem_SL2 📖	mathematical	—	Matrix.GeneralLinearGroup Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction instGLAction DFunLike.coe MonoidHom Matrix.SpecialLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass MonoidHom.instFunLike Matrix.SpecialLinearGroup.mapGL infty	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass one_smul PrincipalIdealRing.to_uniqueFactorizationMonoid IsCoprime.exists_SL2_col IsRelPrime.isCoprime IsBezout.span_pair_isPrincipal IsBezout.of_isPrincipalIdealRing IsFractionRing.num_den_reduced smul_infty_eq_ite Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsLocalRing.toNontrivial Field.instIsLocalRing FaithfulSMul.to_isTorsionFree IsFractionRing.instFaithfulSMul IsDomain.toNontrivial instIsDomain IsFractionRing.mk'_num_den'

Subgroup

Definitions

Name	Category	Theorems
IsRegularAtInfty 📖	MathDef	2 math math: isRegularAtInfty_iff, isRegularAtInfty_of_neg_one_mem
periods 📖	CompOp	8 math math: IsRegularAtInfty.eq, commensurable_strictPeriods_periods, strictPeriods_eq_periods_of_neg_one_mem, relIndex_strictPeriods, strictPeriods_le_periods, widthInfty_mem_periods, instDiscreteTopPeriods, periods_eq_zmultiples_widthInfty
strictPeriods 📖	CompOp	17 math math: IsRegularAtInfty.eq, isRegularAtInfty_iff, CongruenceSubgroup.strictPeriods_Gamma0, ModularFormClass.one_mem_strictPeriods_SL2Z, two_mul_withInfty_mem_strictPeriods, strictPeriods_eq_zmultiples_one_of_T_mem, commensurable_strictPeriods_periods, strictPeriods_eq_periods_of_neg_one_mem, instDiscreteTopStrictPeriods, relIndex_strictPeriods, strictPeriods_le_periods, CongruenceSubgroup.strictPeriods_Gamma1, strictWidthInfty_mem_strictPeriods, CongruenceSubgroup.strictPeriods_Gamma, strictPeriods_SL2Z, mem_strictPeriods_iff, strictPeriods_eq_zmultiples_strictWidthInfty
strictWidthInfty 📖	CompOp	13 math math: CuspFormClass.qExpansion_isBigO, strictWidthInfty_eq_one_of_T_mem, CongruenceSubgroup.strictWidthInfty_Gamma0, CongruenceSubgroup.strictWidthInfty_Gamma1, strictWidthInfty_nonneg, CongruenceSubgroup.strictWidthInfty_Gamma, strictWidthInfty_mem_strictPeriods, ModularFormClass.qExpansion_isBigO, strictWidthInfty_pos_iff, strictWidthInfty_pos, strictPeriods_eq_zmultiples_strictWidthInfty, strictWidthInfty_SL2Z, qExpansion_coeff_isBigO_of_norm_isBigO
widthInfty 📖	CompOp	7 math math: isRegularAtInfty_iff, widthInfty_pos, two_mul_withInfty_mem_strictPeriods, widthInfty_nonneg, widthInfty_pos_iff, widthInfty_mem_periods, periods_eq_zmultiples_widthInfty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commensurable_strictPeriods_periods 📖	mathematical	—	AddSubgroup.Commensurable AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne strictPeriods periods	—	relIndex_strictPeriods Nat.instCharZero Nat.instAtLeastTwoHAddOfNat AddSubgroup.relIndex_eq_one strictPeriods_le_periods
instDiscreteTopPeriods 📖	mathematical	—	DiscreteTopology AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SetLike.instMembership AddSubgroup.instSetLike periods instTopologicalSpaceSubtype	—	instDiscreteTopStrictPeriods instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space
instDiscreteTopStrictPeriods 📖	mathematical	—	DiscreteTopology AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SetLike.instMembership AddSubgroup.instSetLike strictPeriods instTopologicalSpaceSubtype	—	DiscreteTopology.of_subset Set.inter_subset_left DiscreteTopology.of_continuous_injective Continuous.restrict Matrix.GeneralLinearGroup.continuous_upperRightHom Function.Injective.injOn Matrix.GeneralLinearGroup.injective_upperRightHom
isCusp_of_mem_strictPeriods 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike strictPeriods	IsCusp OnePoint.infty	—	mem_strictPeriods_iff Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular LT.lt.ne' OnePoint.smul_infty_eq_self_iff
isRegularAtInfty_iff 📖	mathematical	—	IsRegularAtInfty Real Real.instRing AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SetLike.instMembership AddSubgroup.instSetLike strictPeriods widthInfty	—	widthInfty_mem_periods LE.le.antisymm strictPeriods_le_periods periods_eq_zmultiples_widthInfty AddSubgroup.zmultiples_le
isRegularAtInfty_of_neg_one_mem 📖	mathematical	Matrix.GeneralLinearGroup Fin.fintype Ring.toSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership instSetLike Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg Matrix.nonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units.instOne	IsRegularAtInfty	—	strictPeriods_eq_periods_of_neg_one_mem
mem_strictPeriods_iff 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SetLike.instMembership AddSubgroup.instSetLike strictPeriods Matrix.GeneralLinearGroup Fin.fintype Ring.toSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring instSetLike DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Units.instMonoid AddChar.instFunLike Matrix.GeneralLinearGroup.upperRightHom	—	—
periods_eq_zmultiples_widthInfty 📖	mathematical	—	periods Real Real.instRing AddSubgroup.zmultiples Real.instAddGroup widthInfty	—	strictPeriods_eq_zmultiples_strictWidthInfty
relIndex_strictPeriods 📖	mathematical	—	AddSubgroup.relIndex AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne strictPeriods periods	—	AddSubgroup.relIndex_self Nat.instCharZero Nat.instAtLeastTwoHAddOfNat LE.le.lt_of_ne strictPeriods_le_periods SetLike.lt_iff_le_and_exists instIsConcreteLE AddSubgroup.relIndex_eq_two_iff_exists_notMem_and AddChar.map_add_eq_mul neg_mul_neg MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass instSubgroupClass
strictPeriods_SL2Z 📖	mathematical	—	strictPeriods Real Real.instRing MonoidHom.range Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Ring.toSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra AddSubgroup.zmultiples AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instOne	—	MonoidHom.range_eq_map strictPeriods_eq_zmultiples_one_of_T_mem mem_top
strictPeriods_eq_periods_of_neg_one_mem 📖	mathematical	Matrix.GeneralLinearGroup Fin.fintype Ring.toSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership instSetLike Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg Matrix.nonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units.instOne	strictPeriods periods	—	adjoinNegOne_eq_self_iff
strictPeriods_eq_zmultiples_one_of_T_mem 📖	mathematical	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership instSetLike ModularGroup.T	strictPeriods Real Real.instRing map Matrix.GeneralLinearGroup Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra AddSubgroup.zmultiples AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instOne	—	AddSubgroup.ext zsmul_eq_mul mul_one Matrix.cons_val' Matrix.cons_val_fin_one zpow_mem instSubgroupClass Matrix.ext Fintype.complete ModularGroup.coe_T_zpow Int.cast_one Int.cast_zero
strictPeriods_eq_zmultiples_strictWidthInfty 📖	mathematical	—	strictPeriods Real Real.instRing AddSubgroup.zmultiples Real.instAddGroup strictWidthInfty	—	zmultiples_abs Real.instIsOrderedAddMonoid AddSubgroup.isAddCyclic_iff_exists_zmultiples_eq_top AddSubgroup.discrete_iff_addCyclic instOrderTopologyReal Real.instArchimedean
strictPeriods_le_periods 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder strictPeriods periods	—	le_adjoinNegOne
strictWidthInfty_SL2Z 📖	mathematical	—	strictWidthInfty MonoidHom.range Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing Real.instOne	—	MonoidHom.range_eq_map strictWidthInfty_eq_one_of_T_mem mem_top
strictWidthInfty_eq_one_of_T_mem 📖	mathematical	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership instSetLike ModularGroup.T	strictWidthInfty map Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing Real.instOne	—	strictPeriods_eq_zmultiples_one_of_T_mem AddSubgroup.instDiscreteTopologyZMultiples Real.instIsOrderedAddMonoid instOrderTopologyReal AddSubgroup.zmultiples_eq_zmultiples_iff not_isOfFinAddOrder_of_isAddTorsionFree instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add one_ne_zero NeZero.one Real.instNontrivial strictPeriods_eq_zmultiples_strictWidthInfty
strictWidthInfty_mem_strictPeriods 📖	mathematical	—	Real AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike strictPeriods strictWidthInfty	—	strictPeriods_eq_zmultiples_strictWidthInfty AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass AddSubgroup.instAddSubgroupClass
strictWidthInfty_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero strictWidthInfty	—	IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
strictWidthInfty_pos 📖	mathematical	—	Real Real.instLT Real.instZero strictWidthInfty	—	strictWidthInfty_pos_iff instDiscreteTopStrictPeriods instIsTopologicalRingReal IsArithmetic.discreteTopology instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic OnePoint.map_infty
strictWidthInfty_pos_iff 📖	mathematical	—	Real Real.instLT Real.instZero strictWidthInfty IsCusp OnePoint.infty	—	mem_strictPeriods_iff strictWidthInfty_mem_strictPeriods Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular Matrix.cons_val' Matrix.cons_val_fin_one LT.lt.ne' LE.le.lt_of_ne' strictWidthInfty_nonneg AddSubgroup.zmultiples_ne_bot HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular Real.instIsStrictOrderedRing OnePoint.smul_infty_eq_self_iff AddChar.map_nsmul_eq_pow neg_sq pow_mem SubgroupClass.toSubmonoidClass instSubgroupClass
two_mul_withInfty_mem_strictPeriods 📖	mathematical	—	Real AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike strictPeriods Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat widthInfty	—	widthInfty_mem_periods Nat.instAtLeastTwoHAddOfNat nsmul_eq_mul pow_mem Even.neg_pow
widthInfty_mem_periods 📖	mathematical	—	Real AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike periods widthInfty	—	strictWidthInfty_mem_strictPeriods
widthInfty_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero widthInfty	—	strictWidthInfty_nonneg
widthInfty_pos 📖	mathematical	—	Real Real.instLT Real.instZero widthInfty	—	strictWidthInfty_pos instIsArithmeticAdjoinNegOne
widthInfty_pos_iff 📖	mathematical	—	Real Real.instLT Real.instZero widthInfty IsCusp OnePoint.infty	—	widthInfty.eq_1 strictWidthInfty_pos_iff instHasDetPlusMinusOneAdjoinNegOne Commensurable.isCusp_iff commensurable_adjoinNegOne_self

Subgroup.Commensurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCusp_iff 📖	mathematical	Subgroup.Commensurable Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring	IsCusp	—	isCusp_iff_of_relIndex_ne_zero inf_le_left Subgroup.inf_relIndex_left inf_le_right Subgroup.inf_relIndex_right

Subgroup.HasDetPlusMinusOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isParabolic_iff_of_upperTriangular 📖	mathematical	Matrix.GeneralLinearGroup Fin.fintype DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Units.val MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Matrix.GeneralLinearGroup.IsParabolic DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Ring.toSemiring Units.instMonoid AddChar.instFunLike Matrix.GeneralLinearGroup.upperRightHom Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg Matrix.nonUnitalNonAssocRing	—	Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular_of_det det_eq

Subgroup.IsArithmetic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCusp_iff_isCusp_SL2Z 📖	mathematical	—	IsCusp MonoidHom.range Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing	—	Subgroup.Commensurable.isCusp_iff is_commensurable

Subgroup.IsRegularAtInfty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	Subgroup.IsRegularAtInfty	Subgroup.strictPeriods Subgroup.periods	—	—

(root)

Definitions

Name	Category	Theorems
CuspOrbits 📖	CompOp	2 math math: instFiniteCuspOrbitsOfIsArithmetic, surjective_cosetToCuspOrbit
IsCusp 📖	MathDef	12 math math: Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff', Subgroup.Commensurable.isCusp_iff, Commensurable.isCusp_iff, isCusp_iff_of_relindex_ne_zero, instFactIsCuspInftyRealOfIsArithmetic, isCusp_SL2Z_iff, cosetToCuspOrbit_apply_mk, isCusp_iff_of_relIndex_ne_zero, Subgroup.strictWidthInfty_pos_iff, Subgroup.isCusp_of_mem_strictPeriods, Subgroup.widthInfty_pos_iff
cosetToCuspOrbit 📖	CompOp	2 math math: surjective_cosetToCuspOrbit, cosetToCuspOrbit_apply_mk
cusps_subMulAction 📖	CompOp	1 math math: cosetToCuspOrbit_apply_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cosetToCuspOrbit_apply_mk 📖	mathematical	—	cosetToCuspOrbit Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing QuotientGroup.leftRel Matrix.SpecialLinearGroup.instGroup Subgroup.comap Matrix.GeneralLinearGroup Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Ring.toIntAlgebra Real.instRing OnePoint SubMulAction Real.semiring Subgroup SetLike.instMembership Subgroup.instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction MulAction.instMulAction OnePoint.instGLAction Real.instField Real.decidableEq SubMulAction.instSetLike cusps_subMulAction MulAction.orbitRel SubMulAction.mulAction Units.instMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass MonoidHom.instFunLike Matrix.SpecialLinearGroup.hasInv OnePoint.infty IsCusp MonoidHom.range Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z Set Set.instMembership Set.range OnePoint.map Real.instRatCast isCusp_SL2Z_iff Rat.commRing Rat.instField NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField	—	—
instFiniteCuspOrbitsOfIsArithmetic 📖	mathematical	—	Finite CuspOrbits	—	Finite.of_surjective Subgroup.finite_quotient_of_finiteIndex Subgroup.IsArithmetic.finiteIndex_comap surjective_cosetToCuspOrbit
isCusp_SL2Z_iff 📖	mathematical	—	IsCusp MonoidHom.range Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing OnePoint Set Set.instMembership Set.range OnePoint.map Real.instRatCast	—	Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff ZeroLEOneClass.neZero.two Real.instZeroLEOneClass NeZero.one Real.instNontrivial IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.instAtLeastTwoHAddOfNat Rat.instCharZero Rat.cast_div RCLike.charZero_rclike Rat.cast_sub Rat.cast_intCast Rat.cast_mul Rat.cast_ofNat OnePoint.exists_mem_SL2 Int.instIsDomain Rat.isFractionRing EuclideanDomain.to_principal_ideal_domain zero_ne_one' Matrix.diagonal_apply_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 Matrix.cons_val' Matrix.cons_val_fin_one Int.cast_one Matrix.discr_fin_two Matrix.trace_fin_two Matrix.det_fin_two mul_one Int.cast_zero MulZeroClass.mul_zero sub_zero Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass map_inv Rat.coe_castHom RingHom.algebraMap_toAlgebra OnePoint.map_smul Matrix.SpecialLinearGroup.map_mapGL AddCommGroup.intIsScalarTower SemigroupAction.mul_smul inv_smul_smul
isCusp_SL2Z_iff' 📖	mathematical	—	IsCusp MonoidHom.range Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing CommSemiring.toSemiring CommRing.toCommSemiring OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid MulAction.toSemigroupAction OnePoint.instGLAction Real.instField Real.decidableEq DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass MonoidHom.instFunLike OnePoint.infty	—	isCusp_SL2Z_iff OnePoint.exists_mem_SL2 Int.instIsDomain Rat.isFractionRing EuclideanDomain.to_principal_ideal_domain RCLike.charZero_rclike Rat.coe_castHom OnePoint.map_smul OnePoint.map_infty RingHom.algebraMap_toAlgebra Matrix.SpecialLinearGroup.map_mapGL AddCommGroup.intIsScalarTower
isCusp_iff_of_relIndex_ne_zero 📖	mathematical	Subgroup Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	IsCusp	—	Subgroup.exists_pow_mem_of_relIndex_ne_zero Subgroup.mem_inf Matrix.GeneralLinearGroup.IsParabolic.pow RCLike.charZero_rclike LT.lt.ne' Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff ZeroLEOneClass.neZero.two Real.instZeroLEOneClass NeZero.one Real.instNontrivial IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Matrix.GeneralLinearGroup.IsParabolic.parabolicFixedPoint_pow
isCusp_iff_of_relindex_ne_zero 📖	mathematical	Subgroup Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	IsCusp	—	isCusp_iff_of_relIndex_ne_zero
surjective_cosetToCuspOrbit 📖	mathematical	—	HasQuotient.Quotient Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup QuotientGroup.instHasQuotientSubgroup Subgroup.comap Matrix.GeneralLinearGroup Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Ring.toIntAlgebra Real.instRing CuspOrbits cosetToCuspOrbit	—	isCusp_SL2Z_iff' Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z isCusp_SL2Z_iff inv_inv

---

← Back to Index