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_indToCoind, coindToInd_of_support_subset_orbit, indCoindIso_hom_hom_toLinearMap, indCoindIso_inv_hom_toLinearMap, 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, indToCoind_coindToInd, instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype, instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype, resIndAdjunction_counit_app, resIndAdjunction_homEquiv_apply, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_unit_app	25
Total	34

AddSubgroup

Definitions

Name	Category	Theorems
FiniteIndex 📖	CompData	32 math math: IsFiniteRelIndex.to_finiteIndex_addSubgroupOf, finiteIndex_of_le, exists_finiteIndex_of_leftCoset_cover_aux, isFiniteRelIndex_iff_finiteIndex, FiniteIndexNormalAddSubgroup.isFiniteIndex', Submodule.exists_finiteIndex_of_cover, exists_finiteIndex_of_leftCoset_cover, finiteIndex_range_nsmulAddMonoidHom_of_fg, exists_index_le_card_of_leftCoset_cover, instFiniteIndex_addSubgroupOf, AddGroup.residuallyFinite_iff_exists_finiteIndex, finiteIndex_iInf, finite_iff_finite_and_finiteIndex, instFiniteIndexTop, finiteIndex_toSubgroup_iff, finiteIndex_of_finite_quotient, FiniteIndexNormalAddSubgroup.instFiniteIndex, leftCoset_cover_filter_FiniteIndex_aux, finiteIndex_iff, IsComplement.finite_right_iff, finiteIndex_iff_finite_quotient, finiteIndex_ker, Subgroup.finiteIndex_toAddSubgroup_iff, finiteIndex_iInf', finiteIndex_normalCore, 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	5 math math: coindToInd_of_support_subset_orbit, coindToInd_indToCoind, coindToInd_apply, indCoindIso_inv_hom_toLinearMap, indToCoind_coindToInd
indCoindIso 📖	CompOp	12 math math: coindResAdjunction_counit_app, indCoindNatIso_hom_app, coindResAdjunction_unit_app, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, coindResAdjunction_homEquiv_apply, resIndAdjunction_counit_app, indCoindNatIso_inv_app, coindResAdjunction_homEquiv_symm_apply, indCoindIso_hom_hom_toLinearMap, indCoindIso_inv_hom_toLinearMap, resIndAdjunction_unit_app
indCoindNatIso 📖	CompOp	2 math math: indCoindNatIso_hom_app, indCoindNatIso_inv_app
indToCoind 📖	CompOp	4 math math: coindToInd_indToCoind, indCoindIso_hom_hom_toLinearMap, indCoindIso_inv_hom_toLinearMap, indToCoind_coindToInd
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 CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Functor.comp Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup resFunctor Subgroup.subtype coindFunctor CategoryTheory.Functor.id CategoryTheory.Adjunction.counit coindResAdjunction CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct coind res ind CategoryTheory.Functor.obj CategoryTheory.Iso.inv indCoindIso indFunctor indResAdjunction	—	—
coindResAdjunction_homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup coindFunctor Subgroup.subtype resFunctor EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv coindResAdjunction LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ind res AddCommGroup.toAddCommMonoid instAddCommGroupHom instModuleHom DFinsupp.instEquivLikeLinearEquiv indResHomEquiv CategoryTheory.CategoryStruct.comp coind CategoryTheory.Iso.hom indCoindIso	—	—
coindResAdjunction_homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj resFunctor Subgroup.subtype coindFunctor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv coindResAdjunction CategoryTheory.CategoryStruct.comp coind ind CategoryTheory.Iso.inv indCoindIso LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids res AddCommGroup.toAddCommMonoid instAddCommGroupHom instModuleHom DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm indResHomEquiv	—	RingHomInvPair.ids CategoryTheory.Adjunction.homEquiv_ofNatIsoLeft_symm_apply CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
coindResAdjunction_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp coindFunctor Subgroup.subtype resFunctor CategoryTheory.Adjunction.unit coindResAdjunction CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj indFunctor coind indResAdjunction CategoryTheory.Functor.map CategoryTheory.Iso.hom ind indCoindIso	—	hom_ext Representation.IntertwiningMap.ext LinearMap.ext smulCommClass_self Finsupp.linearCombination_single one_smul
coindToInd_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring V DivInvMonoid.toMonoid Group.toDivInvMonoid coind Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subtype ind Submodule.addCommMonoid Pi.addCommMonoid AddCommGroup.toAddCommMonoid hV1 Pi.Function.module hV2 Representation.coindV ρ Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing 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_indToCoind 📖	mathematical	—	LinearMap.comp V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid coind Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subtype ind Submodule.addCommMonoid Pi.addCommMonoid AddCommGroup.toAddCommMonoid hV1 Pi.Function.module hV2 Representation.coindV ρ Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.instModule Representation.tprod MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular Submodule.module Representation.Coinvariants.instModule RingHomCompTriple.ids indToCoind coindToInd LinearMap.id	—	LinearMap.ext RingHomCompTriple.ids coindToInd_apply Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Submodule.addSubmonoidClass AddSubmonoidClass.coe_finset_sum Finset.sum_apply Finset.sum_eq_single smulCommClass_self Finsupp.linearCombination_single one_smul indToCoindAux_of_not_rel indToCoindAux_self instIsEmptyFalse
coindToInd_of_support_subset_orbit 📖	mathematical	Set Set.instHasSubset Function.support V Subgroup SetLike.instMembership Subgroup.instSetLike CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid hV1 Submodule Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module hV2 Submodule.setLike Representation.coindV Subgroup.subtype ρ MulAction.orbit SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Subgroup.instMulAction Monoid.toMulAction	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring V DivInvMonoid.toMonoid Group.toDivInvMonoid coind Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subtype ind Submodule.addCommMonoid Pi.addCommMonoid AddCommGroup.toAddCommMonoid hV1 Pi.Function.module hV2 Representation.coindV ρ Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing 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 Submodule Submodule.setLike	—	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_toLinearMap 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap Representation.IndV Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subtype V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid hV1 hV2 ρ Submodule Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module Submodule.setLike Representation.coindV Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.instModule Representation.tprod MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular Submodule.addCommGroup Pi.addCommGroup Representation.Coinvariants.instModule Submodule.module Representation.ind Representation.coind Hom.hom of CategoryTheory.Iso.hom Rep instCategory ind coind indCoindIso indToCoind	—	—
indCoindIso_inv_hom_toLinearMap 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid V Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid hV1 Pi.Function.module hV2 Submodule.setLike Representation.coindV Subgroup.subtype ρ Representation.IndV Submodule.addCommGroup CommRing.toRing Pi.addCommGroup Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup TensorProduct.instModule Representation.tprod MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular Submodule.module Representation.Coinvariants.instModule Representation.coind Representation.ind Hom.hom of CategoryTheory.Iso.inv Rep instCategory ind coind indCoindIso LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm Representation.Equiv.toLinearEquiv LinearEquiv.ofLinear indToCoind coindToInd coindToInd_indToCoind indToCoind_coindToInd	—	—
indCoindNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup instCategory 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 CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup instCategory 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 V Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid hV1 Pi.addCommMonoid hV2 Pi.Function.module LinearMap.instFunLike indToCoindAux Representation.IntertwiningMap ρ Representation.IntertwiningMap.instFunLike 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 Representation.IntertwiningMap.instLinearMapClass
indToCoindAux_fst_mul_inv 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring V Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid hV1 Pi.addCommMonoid hV2 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 V Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid hV1 Pi.addCommMonoid hV2 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 V Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid hV1 Pi.addCommMonoid hV2 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 V Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid hV1 Pi.addCommMonoid hV2 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 V Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid hV1 Pi.addCommMonoid hV2 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 V Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup AddCommGroup.toAddCommMonoid hV1 Pi.addCommMonoid hV2 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
indToCoind_coindToInd 📖	mathematical	—	LinearMap.comp V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid ind Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subtype coind AddCommGroup.toAddCommMonoid Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid hV1 Finsupp.module Semiring.toModule hV2 TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.instModule Representation.tprod MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular ρ Submodule.addCommMonoid Pi.addCommMonoid Pi.Function.module Representation.coindV Representation.Coinvariants.instModule Submodule.module RingHomCompTriple.ids coindToInd indToCoind LinearMap.id	—	Representation.Coinvariants.hom_ext RingHomCompTriple.ids TensorProduct.AlgebraTensorModule.curry_injective Finsupp.isScalarTower IsScalarTower.right IsScalarTower.left Finsupp.lhom_ext' IsScalarTower.to_smulCommClass LinearMap.ext_ring LinearMap.ext coindToInd_of_support_subset_orbit Mathlib.Tactic.Contrapose.contrapose₁ smulCommClass_self Finsupp.linearCombination_single one_smul indToCoindAux_of_not_rel indToCoindAux_self
instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup instCategory coindFunctor Subgroup.subtype	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup indFunctor Subgroup.subtype	—	CategoryTheory.Adjunction.isRightAdjoint
resIndAdjunction_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup instCategory CategoryTheory.Functor.comp indFunctor Subgroup.subtype resFunctor CategoryTheory.Functor.id CategoryTheory.Adjunction.counit resIndAdjunction CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj ind coind CategoryTheory.Functor.map CategoryTheory.Iso.hom indCoindIso coindFunctor resCoindAdjunction	—	—
resIndAdjunction_homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj resFunctor Subgroup.subtype indFunctor EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv resIndAdjunction CategoryTheory.CategoryStruct.comp coind ind LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids res AddCommGroup.toAddCommMonoid instAddCommGroupHom instModuleHom DFinsupp.instEquivLikeLinearEquiv resCoindHomEquiv CategoryTheory.Iso.inv indCoindIso	—	RingHomInvPair.ids resIndAdjunction.eq_1 CategoryTheory.Adjunction.homEquiv_ofNatIsoRight_apply CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
resIndAdjunction_homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup indFunctor Subgroup.subtype resFunctor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv resIndAdjunction LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids coind res AddCommGroup.toAddCommMonoid instAddCommGroupHom instModuleHom DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm resCoindHomEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom ind indCoindIso	—	—
resIndAdjunction_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup resFunctor Subgroup.subtype indFunctor CategoryTheory.Adjunction.unit resIndAdjunction CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj coindFunctor ind res resCoindAdjunction CategoryTheory.Iso.inv coind indCoindIso	—	—

Subgroup

Definitions

Name	Category	Theorems
FiniteIndex 📖	CompData	41 math math: CongruenceSubgroup.instFiniteIndexGamma, not_finiteIndex_iff, finiteIndex_center, isFiniteRelIndex_iff_finiteIndex, finiteIndex_iInf, 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', finiteIndex_range_powMonoidHom_of_fg, instFiniteIndexTop, exists_index_le_card_of_leftCoset_cover, isArithmetic_iff_finiteIndex, finiteIndex_of_finite, finiteIndex_iInf', 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, AddSubgroup.finiteIndex_toSubgroup_iff, exists_finiteIndex_of_leftCoset_cover_aux, Group.residuallyFinite_iff_exists_finiteIndex, NumberField.Units.isMaxRank_iff_closure_finiteIndex, CongruenceSubgroup.IsCongruenceSubgroup.finiteIndex, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, IsArithmetic.finiteIndex_comap, finiteIndex_iff, finiteIndex_toAddSubgroup_iff, IsComplement.finite_left_iff, exists_finiteIndex_of_leftCoset_cover, finiteIndex_normalCore, finiteIndex_of_finite_quotient

---

← Back to Index