ArithmeticSubgroups

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

Statistics

Metric	Count
Definitions term𝒮ℒ, HasDetOne, HasDetPlusMinusOne, IsArithmetic, adjoinNegOne, instCoeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupReal	6
Theorems discreteSpecialLinearGroupIntRange, isClosedEmbedding_mapGLInt, det_eq, abs_det, det_eq, discreteTopology, finiteIndex_comap, inter, isFiniteRelIndexSL, is_commensurable, adjoinNegOne_eq_self_iff, commensurable_adjoinNegOne_self, hasDetOne_adjoinNegOne_iff, hasDetPlusMinusOne_adjoinNegOne_iff, hasDetPlusMinusOne_iff_abs_det, instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL, instHasDetOneMapSpecialLinearGroupGeneralLinearGroupToGL, instHasDetOneMinGeneralLinearGroup, instHasDetOneMinGeneralLinearGroup_1, instHasDetOneRangeSpecialLinearGroupGeneralLinearGroupMapGL, instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic, instHasDetPlusMinusOneOfHasDetOne, instIsArithmeticAdjoinNegOne, instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex, instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL, isArithmetic_iff_finiteIndex, le_adjoinNegOne, mem_adjoinNegOne_iff, negOne_mem_adjoinNegOne, relIndex_adjoinNegOne_ne_zero, relindex_adjoinNegOne_eq_two, instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space, instHasDetOneAdjoinNegOneOfFactEvenNatCard, instHasDetPlusMinusOneAdjoinNegOne, instIsFiniteRelIndexGeneralLinearGroupAdjoinNegOne	35
Total	41

Matrix.SpecialLinearGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discreteSpecialLinearGroupIntRange 📖	mathematical	—	DiscreteTopology Matrix.GeneralLinearGroup Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike MonoidHom.range Matrix.SpecialLinearGroup Int.instCommRing instGroup mapGL Ring.toIntAlgebra Real.instRing instTopologicalSpaceSubtype Units.instTopologicalSpaceUnits instTopologicalSpaceMatrix UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Homeomorph.discreteTopology instDiscreteTopology instDiscreteTopologyInt isEmbedding_mapGL instIsTopologicalRingReal Isometry.isEmbedding
isClosedEmbedding_mapGLInt 📖	mathematical	—	Topology.IsClosedEmbedding Matrix.SpecialLinearGroup Int.instCommRing Matrix.GeneralLinearGroup Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing instTopologicalSpace instTopologicalSpaceInt Units.instTopologicalSpaceUnits Matrix instTopologicalSpaceMatrix UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass MonoidHom.instFunLike mapGL Ring.toIntAlgebra Real.instRing	—	isEmbedding_mapGL instIsTopologicalRingReal Isometry.isEmbedding Subgroup.isClosed_of_discrete Units.instIsTopologicalGroupOfContinuousMul instContinuousMulMatrixOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Units.instT2Space instT2SpaceMatrix TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity discreteSpecialLinearGroupIntRange

MatrixGroups

Definitions

Name	Category	Theorems
term𝒮ℒ 📖	CompOp	—

Subgroup

Definitions

Name	Category	Theorems
HasDetOne 📖	CompData	7 math math: instHasDetOneRangeSpecialLinearGroupGeneralLinearGroupMapGL, instHasDetOneMapSpecialLinearGroupGeneralLinearGroupToGL, instHasDetOneMinGeneralLinearGroup_1, instHasDetOneMinGeneralLinearGroup, hasDetOne_adjoinNegOne_iff, instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL, instHasDetOneAdjoinNegOneOfFactEvenNatCard
HasDetPlusMinusOne 📖	CompData	5 math math: instHasDetPlusMinusOneOfHasDetOne, hasDetPlusMinusOne_adjoinNegOne_iff, instHasDetPlusMinusOneAdjoinNegOne, instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic, hasDetPlusMinusOne_iff_abs_det
IsArithmetic 📖	CompData	7 math math: IsArithmetic.inter, instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL, instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex, instIsArithmeticAdjoinNegOne, CongruenceSubgroup.isArithmetic_conj_SL2Z, isArithmetic_iff_finiteIndex, IsArithmetic.conj
adjoinNegOne 📖	CompOp	13 math math: adjoinNegOne_eq_self_iff, mem_adjoinNegOne_iff, hasDetPlusMinusOne_adjoinNegOne_iff, commensurable_adjoinNegOne_self, instIsArithmeticAdjoinNegOne, negOne_mem_adjoinNegOne, instHasDetPlusMinusOneAdjoinNegOne, instIsFiniteRelIndexGeneralLinearGroupAdjoinNegOne, relindex_adjoinNegOne_eq_two, le_adjoinNegOne, hasDetOne_adjoinNegOne_iff, instHasDetOneAdjoinNegOneOfFactEvenNatCard, instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space
instCoeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupReal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoinNegOne_eq_self_iff 📖	mathematical	—	adjoinNegOne Matrix.GeneralLinearGroup 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	—	negOne_mem_adjoinNegOne LE.le.antisymm' le_adjoinNegOne mul_neg neg_mul one_mul neg_neg MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass instSubgroupClass
commensurable_adjoinNegOne_self 📖	mathematical	—	Commensurable Matrix.GeneralLinearGroup Ring.toSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring adjoinNegOne	—	relIndex_eq_one le_adjoinNegOne relIndex_adjoinNegOne_ne_zero
hasDetOne_adjoinNegOne_iff 📖	mathematical	Even Fintype.card	HasDetOne adjoinNegOne CommRing.toRing	—	HasDetOne.det_eq le_adjoinNegOne Matrix.det_neg Even.neg_pow one_pow one_mul
hasDetPlusMinusOne_adjoinNegOne_iff 📖	mathematical	—	HasDetPlusMinusOne adjoinNegOne CommRing.toRing	—	HasDetPlusMinusOne.det_eq le_adjoinNegOne Matrix.det_neg Even.neg_pow one_pow one_mul Odd.neg_one_pow Nat.not_even_iff_odd neg_mul neg_neg
hasDetPlusMinusOne_iff_abs_det 📖	mathematical	—	HasDetPlusMinusOne abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	HasDetPlusMinusOne.abs_det abs_eq zero_le_one IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL 📖	mathematical	—	HasDetOne map Matrix.SpecialLinearGroup Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL	—	Matrix.SpecialLinearGroup.det_mapGL
instHasDetOneMapSpecialLinearGroupGeneralLinearGroupToGL 📖	mathematical	—	HasDetOne map Matrix.SpecialLinearGroup Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.toGL	—	Matrix.SpecialLinearGroup.coeToGL_det
instHasDetOneMinGeneralLinearGroup 📖	mathematical	—	HasDetOne Subgroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring instMin	—	HasDetOne.det_eq
instHasDetOneMinGeneralLinearGroup_1 📖	mathematical	—	HasDetOne Subgroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring instMin	—	HasDetOne.det_eq
instHasDetOneRangeSpecialLinearGroupGeneralLinearGroupMapGL 📖	mathematical	—	HasDetOne MonoidHom.range Matrix.SpecialLinearGroup Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL	—	Matrix.SpecialLinearGroup.det_mapGL
instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic 📖	mathematical	—	HasDetPlusMinusOne Fin.fintype Real Real.commRing	—	hasDetPlusMinusOne_iff_abs_det Real.instIsOrderedRing exists_pow_mem_of_relIndex_ne_zero IsArithmetic.is_commensurable map_pow MonoidHom.instMonoidHomClass Matrix.SpecialLinearGroup.det_mapGL abs_one abs_pow_eq_one Real.instIsStrictOrderedRing
instHasDetPlusMinusOneOfHasDetOne 📖	mathematical	—	HasDetPlusMinusOne	—	HasDetOne.det_eq
instIsArithmeticAdjoinNegOne 📖	mathematical	—	IsArithmetic adjoinNegOne Fin.fintype Real Real.instRing	—	Commensurable.trans commensurable_adjoinNegOne_self IsArithmetic.is_commensurable
instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex 📖	mathematical	—	IsArithmetic 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	—	isArithmetic_iff_finiteIndex
instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL 📖	mathematical	—	IsArithmetic 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	—	Commensurable.refl
isArithmetic_iff_finiteIndex 📖	mathematical	—	IsArithmetic 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 FiniteIndex	—	MonoidHom.range_eq_map comap_map_eq_self_of_injective Matrix.SpecialLinearGroup.mapGL_injective instFaithfulSMulIntOfCharZero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing relIndex_top_right relIndex_top_left
le_adjoinNegOne 📖	mathematical	—	Subgroup Matrix.GeneralLinearGroup Ring.toSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Preorder.toLE PartialOrder.toPreorder instPartialOrder adjoinNegOne	—	—
mem_adjoinNegOne_iff 📖	mathematical	—	Matrix.GeneralLinearGroup Ring.toSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership instSetLike adjoinNegOne Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg Matrix.nonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
negOne_mem_adjoinNegOne 📖	mathematical	—	Matrix.GeneralLinearGroup Ring.toSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership instSetLike adjoinNegOne Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg Matrix.nonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units.instOne	—	neg_neg SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass instSubgroupClass
relIndex_adjoinNegOne_ne_zero 📖	—	—	—	—	adjoinNegOne_eq_self_iff relIndex_self relindex_adjoinNegOne_eq_two Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
relindex_adjoinNegOne_eq_two 📖	mathematical	Matrix.GeneralLinearGroup 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	relIndex Matrix.GeneralLinearGroup Ring.toSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring adjoinNegOne	—	relIndex_eq_two_iff_exists_notMem_and negOne_mem_adjoinNegOne mul_neg mul_one

Subgroup.HasDetOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_eq 📖	mathematical	Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det Units.instOne	—	—

Subgroup.HasDetPlusMinusOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_det 📖	mathematical	Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	det_eq abs_one abs_neg
det_eq 📖	mathematical	Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det Units.instOne Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—

Subgroup.IsArithmetic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discreteTopology 📖	mathematical	—	DiscreteTopology Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike instTopologicalSpaceSubtype Units.instTopologicalSpaceUnits instTopologicalSpaceMatrix UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Subgroup.Commensurable.discreteTopology_iff Units.instIsTopologicalGroupOfContinuousMul instContinuousMulMatrixOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Units.instT2Space instT2SpaceMatrix TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity is_commensurable Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange
finiteIndex_comap 📖	mathematical	—	Subgroup.FiniteIndex Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing 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	—	is_commensurable Subgroup.index_comap
inter 📖	mathematical	—	Subgroup.IsArithmetic Subgroup Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Subgroup.instMin	—	Subgroup.relIndex_inf_ne_zero is_commensurable Subgroup.relIndex_ne_zero_trans Subgroup.relIndex_eq_one inf_le_left
isFiniteRelIndexSL 📖	mathematical	—	Subgroup.IsFiniteRelIndex Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.range Matrix.SpecialLinearGroup Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing	—	is_commensurable
is_commensurable 📖	mathematical	—	Subgroup.Commensurable Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.range Matrix.SpecialLinearGroup Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space 📖	mathematical	—	DiscreteTopology Matrix.GeneralLinearGroup Ring.toSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Subgroup.adjoinNegOne instTopologicalSpaceSubtype Units.instTopologicalSpaceUnits instTopologicalSpaceMatrix	—	Subgroup.Commensurable.discreteTopology_iff Units.instIsTopologicalGroupOfContinuousMul instContinuousMulMatrixOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Units.instT2Space instT2SpaceMatrix Subgroup.commensurable_adjoinNegOne_self
instHasDetOneAdjoinNegOneOfFactEvenNatCard 📖	mathematical	—	Subgroup.HasDetOne Subgroup.adjoinNegOne CommRing.toRing	—	Subgroup.hasDetOne_adjoinNegOne_iff Fact.out
instHasDetPlusMinusOneAdjoinNegOne 📖	mathematical	—	Subgroup.HasDetPlusMinusOne Subgroup.adjoinNegOne CommRing.toRing	—	Subgroup.hasDetPlusMinusOne_adjoinNegOne_iff
instIsFiniteRelIndexGeneralLinearGroupAdjoinNegOne 📖	mathematical	—	Subgroup.IsFiniteRelIndex Matrix.GeneralLinearGroup Ring.toSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Subgroup.adjoinNegOne	—	Subgroup.relIndex_adjoinNegOne_ne_zero

---

← Back to Index