FiniteIndex

📁 Source: Mathlib/RepresentationTheory/FiniteIndex.lean

Statistics

Metric	Count
Definitions FiniteIndex, coindResAdjunction, coindToInd, indCoindIso, indCoindNatIso, indToCoind, indToCoindAux, resIndAdjunction, FiniteIndex	9
Theorems coindResAdjunction_counit_app, coindResAdjunction_homEquiv_apply, coindResAdjunction_homEquiv_symm_apply, coindResAdjunction_unit_app, coindToInd_apply, coindToInd_of_support_subset_orbit, indCoindIso_hom_hom_hom, indCoindIso_inv_hom_hom, indCoindNatIso_hom_app, indCoindNatIso_inv_app, indToCoindAux_comm, indToCoindAux_fst_mul_inv, indToCoindAux_mul_fst, indToCoindAux_mul_snd, indToCoindAux_of_not_rel, indToCoindAux_self, indToCoindAux_snd_mul_inv, instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype, instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype, resIndAdjunction_counit_app, resIndAdjunction_homEquiv_apply, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_unit_app	23
Total	32

AddSubgroup

Definitions

Name	Category	Theorems
FiniteIndex 📖	CompData	24 math math: IsFiniteRelIndex.to_finiteIndex_addSubgroupOf, finiteIndex_of_le, exists_finiteIndex_of_leftCoset_cover_aux, FiniteIndexNormalAddSubgroup.isFiniteIndex', Submodule.exists_finiteIndex_of_cover, exists_finiteIndex_of_leftCoset_cover, exists_index_le_card_of_leftCoset_cover, instFiniteIndex_addSubgroupOf, finite_iff_finite_and_finiteIndex, instFiniteIndexTop, finiteIndex_of_finite_quotient, FiniteIndexNormalAddSubgroup.instFiniteIndex, leftCoset_cover_filter_FiniteIndex_aux, finiteIndex_iff, IsComplement.finite_right_iff, finiteIndex_iff_finite_quotient, finiteIndex_ker, leftCoset_cover_filter_FiniteIndex, instFiniteIndexMin, pairwiseDisjoint_leftCoset_cover_of_sum_neg_index_eq_zero, IsComplement.finite_left_iff, finiteIndex_of_leftCoset_cover_const, finiteIndex_of_finite, not_finiteIndex_iff

Rep

Definitions

Name	Category	Theorems
coindResAdjunction 📖	CompOp	4 math math: coindResAdjunction_counit_app, coindResAdjunction_unit_app, coindResAdjunction_homEquiv_apply, coindResAdjunction_homEquiv_symm_apply
coindToInd 📖	CompOp	3 math math: coindToInd_of_support_subset_orbit, indCoindIso_inv_hom_hom, coindToInd_apply
indCoindIso 📖	CompOp	12 math math: coindResAdjunction_counit_app, indCoindNatIso_hom_app, indCoindIso_inv_hom_hom, indCoindIso_hom_hom_hom, coindResAdjunction_unit_app, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, coindResAdjunction_homEquiv_apply, resIndAdjunction_counit_app, indCoindNatIso_inv_app, coindResAdjunction_homEquiv_symm_apply, resIndAdjunction_unit_app
indCoindNatIso 📖	CompOp	2 math math: indCoindNatIso_hom_app, indCoindNatIso_inv_app
indToCoind 📖	CompOp	1 math math: indCoindIso_hom_hom_hom
indToCoindAux 📖	CompOp	7 math math: indToCoindAux_self, indToCoindAux_fst_mul_inv, indToCoindAux_comm, indToCoindAux_mul_fst, indToCoindAux_mul_snd, indToCoindAux_snd_mul_inv, indToCoindAux_of_not_rel
resIndAdjunction 📖	CompOp	4 math math: resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, resIndAdjunction_counit_app, resIndAdjunction_unit_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coindResAdjunction_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.comp Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Action.res Subgroup.subtype coindFunctor CategoryTheory.Functor.id CategoryTheory.Adjunction.counit coindResAdjunction CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct coind CategoryTheory.Functor.obj Action ind CategoryTheory.Iso.inv indCoindIso indFunctor indResAdjunction	—	CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
coindResAdjunction_homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup coindFunctor Subgroup.subtype Action.res EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv coindResAdjunction LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ind Action AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep DFinsupp.instEquivLikeLinearEquiv indResHomEquiv CategoryTheory.CategoryStruct.comp coind CategoryTheory.Iso.hom indCoindIso	—	RingHomInvPair.ids CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
coindResAdjunction_homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action.res Subgroup.subtype coindFunctor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv coindResAdjunction CategoryTheory.CategoryStruct.comp coind ind CategoryTheory.Iso.inv indCoindIso LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Action AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm indResHomEquiv	—	RingHomInvPair.ids CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
coindResAdjunction_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp coindFunctor Subgroup.subtype Action.res CategoryTheory.Adjunction.unit coindResAdjunction CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj indFunctor Action coind indResAdjunction CategoryTheory.Functor.map CategoryTheory.Iso.hom ind indCoindIso	—	Action.hom_ext ModuleCat.hom_ext LinearMap.ext RingHomCompTriple.ids CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv CategoryTheory.Category.comp_id CategoryTheory.Category.assoc smulCommClass_self Finsupp.linearCombination_single one_smul
coindToInd_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid coind Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subtype ind Submodule.addCommMonoid Pi.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule Representation.coindV ρ Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid ModuleCat.isAddCommGroup Finsupp.module Semiring.toModule TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup TensorProduct.instModule Representation.tprod MonoidHom.comp NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular Submodule.module Representation.Coinvariants.instModule LinearMap.instFunLike coindToInd Finset.sum QuotientGroup.rightRel Finset.univ QuotientGroup.fintypeQuotientRightRel Subgroup.fintypeQuotientOfFiniteIndex Representation.IndV Submodule Submodule.setLike	—	—
coindToInd_of_support_subset_orbit 📖	mathematical	Set Set.instHasSubset Function.support ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupCarrierVModuleCat Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module ModuleCat.isModule Submodule.setLike Representation.coindV Subgroup.subtype ρ MulAction.orbit SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Subgroup.instMulAction Monoid.toMulAction	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring coind ind Submodule.addCommMonoid Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid ModuleCat.isAddCommGroup Finsupp.module Semiring.toModule TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup TensorProduct.instModule Representation.tprod MonoidHom.comp NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular Submodule.module Representation.Coinvariants.instModule LinearMap.instFunLike coindToInd Representation.IndV	—	coindToInd_apply Finset.sum_eq_single Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq TensorProduct.tmul_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass instIsEmptyFalse
indCoindIso_hom_hom_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid ind Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subtype coind Action.Hom.hom CategoryTheory.Iso.hom Rep Action.instCategory indCoindIso indToCoind	—	—
indCoindIso_inv_hom_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid coind Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subtype ind Action.Hom.hom CategoryTheory.Iso.inv Rep Action.instCategory indCoindIso coindToInd	—	—
indCoindNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Action.instCategory ModuleCat ModuleCat.moduleCategory indFunctor Subgroup.subtype coindFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category indCoindNatIso ind coind indCoindIso	—	—
indCoindNatIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Action.instCategory ModuleCat ModuleCat.moduleCategory coindFunctor Subgroup.subtype indFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category indCoindNatIso ind coind indCoindIso	—	—
indToCoindAux_comm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.addCommMonoid ModuleCat.isModule Pi.Function.module LinearMap.instFunLike indToCoindAux CategoryTheory.ConcreteCategory.hom Ring.toSemiring ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom	—	em Submonoid.smul_def indToCoindAux_mul_snd indToCoindAux_self hom_comm_apply indToCoindAux_of_not_rel map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
indToCoindAux_fst_mul_inv 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.addCommMonoid ModuleCat.isModule Pi.Function.module LinearMap.instFunLike indToCoindAux MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_inv indToCoindAux_snd_mul_inv
indToCoindAux_mul_fst 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.addCommMonoid ModuleCat.isModule Pi.Function.module LinearMap.instFunLike indToCoindAux MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Representation MonoidHom.instFunLike MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	em Submonoid.smul_def mul_assoc inv_mul_cancel_left Module.End.mul_apply map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass mul_inv_rev mul_inv_cancel_left mul_inv_cancel mul_one Subtype.coe_eta inv_mul_cancel indToCoindAux_of_not_rel
indToCoindAux_mul_snd 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.addCommMonoid ModuleCat.isModule Pi.Function.module LinearMap.instFunLike indToCoindAux MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Representation MonoidHom.instFunLike MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	em mul_assoc Submonoid.smul_def mul_inv_cancel mul_one map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass Subtype.coe_eta indToCoindAux_of_not_rel inv_mul_cancel_left map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
indToCoindAux_of_not_rel 📖	mathematical	QuotientGroup.rightRel	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.addCommMonoid ModuleCat.isModule Pi.Function.module LinearMap.instFunLike indToCoindAux NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
indToCoindAux_self 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.addCommMonoid ModuleCat.isModule Pi.Function.module LinearMap.instFunLike indToCoindAux	—	indToCoindAux.eq_1 LinearMap.pi_apply Setoid.refl' mul_inv_cancel map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
indToCoindAux_snd_mul_inv 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.addCommMonoid ModuleCat.isModule Pi.Function.module LinearMap.instFunLike indToCoindAux MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	em eq_mul_inv_iff_mul_eq Submonoid.smul_def mul_assoc mul_inv_cancel mul_one indToCoindAux_mul_snd indToCoindAux_self indToCoindAux_of_not_rel
instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Action.instCategory ModuleCat ModuleCat.moduleCategory coindFunctor Subgroup.subtype	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup indFunctor Subgroup.subtype	—	CategoryTheory.Adjunction.isRightAdjoint
resIndAdjunction_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Action ModuleCat CommRing.toRing ModuleCat.moduleCategory Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Action.instCategory CategoryTheory.Functor.comp indFunctor Subgroup.subtype Action.res CategoryTheory.Functor.id CategoryTheory.Adjunction.counit resIndAdjunction CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj ind coind CategoryTheory.Functor.map CategoryTheory.Iso.hom Rep indCoindIso coindFunctor resCoindAdjunction	—	—
resIndAdjunction_homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Action ModuleCat CommRing.toRing ModuleCat.moduleCategory Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res Subgroup.subtype indFunctor EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv resIndAdjunction CategoryTheory.CategoryStruct.comp Rep coind ind LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep DFinsupp.instEquivLikeLinearEquiv resCoindHomEquiv CategoryTheory.Iso.inv indCoindIso	—	RingHomInvPair.ids CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
resIndAdjunction_homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Action ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup indFunctor Subgroup.subtype Action.res EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv resIndAdjunction LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Rep coind AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm resCoindHomEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom ind indCoindIso	—	RingHomInvPair.ids CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
resIndAdjunction_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Action ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Action.res Subgroup.subtype indFunctor CategoryTheory.Adjunction.unit resIndAdjunction CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj coindFunctor ind resCoindAdjunction CategoryTheory.Iso.inv Rep coind indCoindIso	—	—

Subgroup

Definitions

Name	Category	Theorems
FiniteIndex 📖	CompData	34 math math: CongruenceSubgroup.instFiniteIndexGamma, not_finiteIndex_iff, finiteIndex_center, CongruenceSubgroup.instFiniteIndexGamma1, FiniteIndexNormalSubgroup.instFiniteIndex, finite_iff_finite_and_finiteIndex, instFiniteIndexMin, leftCoset_cover_filter_FiniteIndex_aux, instFiniteIndex_subgroupOf, IsComplement.finite_right_iff, finiteIndex_of_leftCoset_cover_const, FiniteIndexNormalSubgroup.isFiniteIndex', instFiniteIndexTop, exists_index_le_card_of_leftCoset_cover, isArithmetic_iff_finiteIndex, finiteIndex_of_finite, CongruenceSubgroup.finiteIndex_conjGL, CongruenceSubgroup.instFiniteIndexGamma0, finiteIndex_ker, IsFiniteRelIndex.to_finiteIndex_subgroupOf, finiteIndex_iff_finite_quotient, finiteIndex_of_le, leftCoset_cover_filter_FiniteIndex, pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one, exists_finiteIndex_of_leftCoset_cover_aux, NumberField.Units.isMaxRank_iff_closure_finiteIndex, CongruenceSubgroup.IsCongruenceSubgroup.finiteIndex, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, IsArithmetic.finiteIndex_comap, finiteIndex_iff, IsComplement.finite_left_iff, exists_finiteIndex_of_leftCoset_cover, finiteIndex_normalCore, finiteIndex_of_finite_quotient

---

← Back to Index