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 IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalSemiring.toContinuousMul 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	8 math math: IsArithmetic.inter, instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL, instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex, instIsArithmeticAdjoinNegOne, CongruenceSubgroup.IsArithmetic.conj, 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 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 Units MulOneClass.toMulOne Units.instMulOneClass 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 DFunLike.coe MonoidHom Units MulOneClass.toMulOne Units.instMulOneClass 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 Units MulOneClass.toMulOne Units.instMulOneClass 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 IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalSemiring.toContinuousMul 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 IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalSemiring.toContinuousMul 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