CongruenceSubgroups

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

Statistics

Metric	Count
Definitions Gamma0, Gamma0Map, Gamma1, Gamma1', IsCongruenceSubgroup, conjGL, «termΓ(_)»»)	7
Theorems Gamma0_is_congruence, Gamma0_mem, Gamma1_in_Gamma0, Gamma1_is_congruence, Gamma1_mem, Gamma1_mem', Gamma1_to_Gamma0_mem, Gamma_cong_eq_self, Gamma_is_cong_sub, Gamma_mem, Gamma_mem', Gamma_normal, Gamma_one_top, Gamma_zero_bot, conj, conjGL, finiteIndex, ModularGroup_T_pow_mem_Gamma, conjGL_coe, conj_cong_is_cong, exists_Gamma_le_conj, exists_Gamma_le_conj', finiteIndex_conjGL, instFiniteIndexGamma, instFiniteIndexGamma0, instFiniteIndexGamma1, isArithmetic_conj_SL2Z, isCongruenceSubgroup_trans, mem_Gamma_one, mem_conjGL, mem_conjGL', SL_reduction_mod_hom_val, conj	33
Total	40

CongruenceSubgroup

Definitions

Name	Category	Theorems
Gamma0 📖	CompOp	8 math math: strictPeriods_Gamma0, Gamma1_mem', strictWidthInfty_Gamma0, instFiniteIndexGamma0, Gamma1_in_Gamma0, Gamma0_is_congruence, Gamma1_to_Gamma0_mem, Gamma0_mem
Gamma0Map 📖	CompOp	1 math math: Gamma1_mem'
Gamma1 📖	CompOp	6 math math: instFiniteIndexGamma1, strictWidthInfty_Gamma1, strictPeriods_Gamma1, Gamma1_in_Gamma0, Gamma1_mem, Gamma1_is_congruence
Gamma1' 📖	CompOp	2 math math: Gamma1_mem', Gamma1_to_Gamma0_mem
IsCongruenceSubgroup 📖	MathDef	3 math math: Gamma_is_cong_sub, Gamma0_is_congruence, Gamma1_is_congruence
conjGL 📖	CompOp	5 math math: conjGL_coe, finiteIndex_conjGL, mem_conjGL, mem_conjGL', IsCongruenceSubgroup.conjGL
«termΓ(_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Gamma0_is_congruence 📖	mathematical	—	IsCongruenceSubgroup Gamma0	—	isCongruenceSubgroup_trans Gamma1_in_Gamma0 Gamma1_is_congruence
Gamma0_mem 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership Subgroup.instSetLike Gamma0 ZMod AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
Gamma1_in_Gamma0 📖	mathematical	—	Subgroup Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Gamma1 Gamma0	—	—
Gamma1_is_congruence 📖	mathematical	—	IsCongruenceSubgroup Gamma1	—	—
Gamma1_mem 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership Subgroup.instSetLike Gamma1 ZMod AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Gamma1_to_Gamma0_mem
Gamma1_mem' 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership Subgroup.instSetLike Gamma0 Subgroup.toGroup Gamma1' DFunLike.coe MonoidHom ZMod MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing MonoidHom.instFunLike Gamma0Map AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
Gamma1_to_Gamma0_mem 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership Subgroup.instSetLike Gamma0 Subgroup.toGroup Gamma1' ZMod AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Int.cast_one Gamma0_mem mul_one MulZeroClass.mul_zero sub_zero Int.cast_sub Int.cast_mul Matrix.det_fin_two
Gamma_cong_eq_self 📖	mathematical	—	ConjAct Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction Gamma	—	Subgroup.Normal.conjAct Gamma_normal
Gamma_is_cong_sub 📖	mathematical	—	IsCongruenceSubgroup Gamma	—	le_rfl
Gamma_mem 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership Subgroup.instSetLike Gamma ZMod AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Gamma_mem' Matrix.one_apply_eq Matrix.one_apply_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 Matrix.SpecialLinearGroup.ext SL_reduction_mod_hom_val Fintype.complete
Gamma_mem' 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership Subgroup.instSetLike Gamma DFunLike.coe MonoidHom ZMod ZMod.commRing MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid MonoidHom.instFunLike Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Matrix.SpecialLinearGroup.hasOne	—	—
Gamma_normal 📖	mathematical	—	Subgroup.Normal Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Gamma	—	MonoidHom.normal_ker
Gamma_one_top 📖	mathematical	—	Gamma Top.top Subgroup Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Subgroup.instTop	—	Subgroup.ext Unique.instSubsingleton
Gamma_zero_bot 📖	mathematical	—	Gamma Bot.bot Subgroup Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Subgroup.instBot	—	—
ModularGroup_T_pow_mem_Gamma 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership Subgroup.instSetLike Gamma DivInvMonoid.toZPow Group.toDivInvMonoid ModularGroup.T	—	ModularGroup.coe_T_zpow Matrix.cons_val' Matrix.empty_val' Matrix.cons_val_fin_one Int.cast_one Int.cast_zero ZMod.intCast_zmod_eq_zero_iff_dvd Int.natCast_natAbs
conjGL_coe 📖	mathematical	—	conjGL DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Fin.fintype Real Real.commRing Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike Matrix.SpecialLinearGroup.toGL Int.instCommRing Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing ConjAct Subgroup Matrix.SpecialLinearGroup.instGroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction MulEquiv MulOne.toMul EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct Matrix.SpecialLinearGroup.hasInv	—	Subgroup.ext MonoidHom.instMonoidHomClass MonoidHomClass.toMulHomClass Matrix.SpecialLinearGroup.toGL_injective Matrix.SpecialLinearGroup.map_intCast_injective IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
conj_cong_is_cong 📖	mathematical	IsCongruenceSubgroup	ConjAct Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction	—	Gamma_cong_eq_self Subgroup.pointwise_smul_le_pointwise_smul_iff
exists_Gamma_le_conj 📖	mathematical	—	Matrix.GeneralLinearGroup Fin.fintype Rat.semiring Subgroup CommSemiring.toSemiring CommRing.toCommSemiring Rat.commRing Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Subgroup.map Matrix.SpecialLinearGroup Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.SpecialLinearGroup.mapGL Ring.toIntAlgebra DivisionRing.toRing Rat.instDivisionRing Gamma Units.instMul DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass MonoidHom.instFunLike Units.instInv	—	mul_inv_cancel mul_ne_zero IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Matrix.den_ne_zero Gamma_mem' sub_eq_iff_eq_add' Matrix.ext nsmul_eq_mul Nat.cast_mul Matrix.map_sub Int.cast_sub sub_eq_zero Matrix.map_one Int.cast_zero Int.cast_one Matrix.map_add Int.cast_add mul_add Distrib.leftDistribClass mul_one add_mul Distrib.rightDistribClass AddLeftCancelSemigroup.toIsLeftCancelAdd Matrix.inv_denom_smul_num Matrix.map_smul Int.cast_mul Int.cast_natCast Matrix.map_mul_intCast Matrix.mul_smul Algebra.to_smulCommClass Matrix.smul_mul IsScalarTower.right Nat.cast_smul_eq_nsmul SemigroupAction.mul_smul mul_comm mul_assoc inv_mul_cancel_left₀ Nat.cast_zero Rat.instCharZero mul_inv_cancel_right₀ one_mul Matrix.det_one Matrix.det_mul mul_right_comm SetLike.mem_coe map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass ZMod.natCast_self MulZeroClass.zero_mul
exists_Gamma_le_conj' 📖	mathematical	—	Subgroup Matrix.GeneralLinearGroup Real Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder 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 MonoidHom Rat.commRing Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.map Rat.castHom Real.instDivisionRing IsStrictOrderedRing.toCharZero Ring.toSemiring DivisionRing.toRing Real.partialOrder Real.instIsStrictOrderedRing Subgroup.map Matrix.SpecialLinearGroup Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.SpecialLinearGroup.mapGL Ring.toIntAlgebra Real.instRing Gamma	—	IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing exists_Gamma_le_conj map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
finiteIndex_conjGL 📖	mathematical	—	Subgroup.FiniteIndex Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup conjGL Top.top Subgroup Subgroup.instTop DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Rat.commRing Real Real.commRing MulOneClass.toMulOne Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.map Rat.castHom Real.instDivisionRing IsStrictOrderedRing.toCharZero Ring.toSemiring DivisionRing.toRing Real.partialOrder Real.instIsStrictOrderedRing	—	IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing exists_Gamma_le_conj' instFaithfulSMulIntOfCharZero MonoidHom.range_eq_map Gamma_one_top Subgroup.smul_mem_pointwise_smul Subgroup.index_comap Subgroup.FiniteIndex.index_ne_zero Subgroup.finiteIndex_of_le instFiniteIndexGamma conjGL.eq_1 Subgroup.inf_relIndex_right
instFiniteIndexGamma 📖	mathematical	—	Subgroup.FiniteIndex Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Gamma	—	Subgroup.finiteIndex_ker Subgroup.instFiniteSubtypeMem Matrix.SpecialLinearGroup.instFinite Finite.of_fintype
instFiniteIndexGamma0 📖	mathematical	—	Subgroup.FiniteIndex Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Gamma0	—	IsCongruenceSubgroup.finiteIndex Gamma0_is_congruence
instFiniteIndexGamma1 📖	mathematical	—	Subgroup.FiniteIndex Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Gamma1	—	IsCongruenceSubgroup.finiteIndex Gamma1_is_congruence
isArithmetic_conj_SL2Z 📖	mathematical	—	Subgroup.IsArithmetic ConjAct Matrix.GeneralLinearGroup Real Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring 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 MonoidHom Rat.commRing Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.map Rat.castHom Real.instDivisionRing IsStrictOrderedRing.toCharZero Ring.toSemiring DivisionRing.toRing Real.partialOrder Real.instIsStrictOrderedRing MonoidHom.range Matrix.SpecialLinearGroup Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.SpecialLinearGroup.mapGL Ring.toIntAlgebra Real.instRing	—	IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing MonoidHom.range_eq_map Subgroup.relIndex_comap Subgroup.relIndex_top_right Subgroup.FiniteIndex.index_ne_zero finiteIndex_conjGL Subgroup.relIndex_pointwise_smul inv_smul_smul
isCongruenceSubgroup_trans 📖	—	Subgroup Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder IsCongruenceSubgroup	—	—	LE.le.trans
mem_Gamma_one 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership Subgroup.instSetLike Gamma	—	Gamma_one_top
mem_conjGL 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership Subgroup.instSetLike conjGL DFunLike.coe MonoidHom Real Real.commRing Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike Matrix.SpecialLinearGroup.toGL Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Real.semiring Units.instMul Units.instInv	—	—
mem_conjGL' 📖	mathematical	—	Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Subgroup Matrix.SpecialLinearGroup.instGroup SetLike.instMembership Subgroup.instSetLike conjGL Matrix.GeneralLinearGroup Real Real.semiring Units.instMul Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Units.instInv DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass MonoidHom.instFunLike Matrix.SpecialLinearGroup.toGL Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing	—	mem_conjGL eq_mul_inv_iff_mul_eq mul_assoc inv_mul_eq_iff_eq_mul

CongruenceSubgroup.IsArithmetic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj 📖	mathematical	—	Subgroup.IsArithmetic ConjAct Matrix.GeneralLinearGroup Real Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Subgroup Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring 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 MonoidHom Rat.commRing Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.map Rat.castHom Real.instDivisionRing IsStrictOrderedRing.toCharZero Ring.toSemiring DivisionRing.toRing Real.partialOrder Real.instIsStrictOrderedRing	—	Subgroup.IsArithmetic.conj

CongruenceSubgroup.IsCongruenceSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjGL 📖	mathematical	CongruenceSubgroup.IsCongruenceSubgroup	CongruenceSubgroup.conjGL DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Rat.commRing Real Real.commRing MulOneClass.toMulOne Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.map Rat.castHom Real.instDivisionRing IsStrictOrderedRing.toCharZero Ring.toSemiring DivisionRing.toRing Real.partialOrder Real.instIsStrictOrderedRing	—	IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing CongruenceSubgroup.exists_Gamma_le_conj' Subgroup.mem_inv_pointwise_smul_iff Subgroup.pointwise_smul_subset_iff CongruenceSubgroup.mem_conjGL
finiteIndex 📖	mathematical	CongruenceSubgroup.IsCongruenceSubgroup	Subgroup.FiniteIndex Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup	—	Subgroup.finiteIndex_of_le CongruenceSubgroup.instFiniteIndexGamma

Subgroup.IsArithmetic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj 📖	mathematical	—	Subgroup.IsArithmetic ConjAct Matrix.GeneralLinearGroup Real Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Subgroup Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring 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 MonoidHom Rat.commRing Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.map Rat.castHom Real.instDivisionRing IsStrictOrderedRing.toCharZero Ring.toSemiring DivisionRing.toRing Real.partialOrder Real.instIsStrictOrderedRing	—	IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Subgroup.Commensurable.trans Subgroup.Commensurable.conj is_commensurable CongruenceSubgroup.isArithmetic_conj_SL2Z

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SL_reduction_mod_hom_val 📖	mathematical	—	Matrix ZMod Matrix.det Fin.fintype ZMod.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe MonoidHom Matrix.SpecialLinearGroup Int.instCommRing MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid MonoidHom.instFunLike Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing AddGroupWithOne.toIntCast	—	—

---

← Back to Index