Induced

📁 Source: Mathlib/RepresentationTheory/Induced.lean

Statistics

Metric	Count
Definitions coinvariantsTensorIndHom, coinvariantsTensorIndInv, coinvariantsTensorIndIso, coinvariantsTensorIndNatIso, ind, indFunctor, indMap, indResAdjunction, indResHomEquiv, IndV, mk, ind	12
Theorems coinvariantsTensorIndHom_mk_tmul_indVMk, coinvariantsTensorIndInv_mk_tmul_indMk, coinvariantsTensorIndIso_hom, coinvariantsTensorIndIso_inv, coinvariantsTensorIndNatIso_hom_app, coinvariantsTensorIndNatIso_inv_app, indFunctor_map, indFunctor_obj, indMap_hom, indResAdjunction_counit_app_hom_hom, indResAdjunction_unit_app_hom_hom, indResHomEquiv_apply_hom, indResHomEquiv_symm_apply_hom, instIsLeftAdjointIndFunctor, instIsRightAdjointActionModuleCatRes, hom_ext, hom_ext_iff, ind_apply, ind_mk	19
Total	31

Rep

Definitions

Name	Category	Theorems
coinvariantsTensorIndHom 📖	CompOp	3 math math: coinvariantsTensorIndIso_hom, coinvariantsTensorIndNatIso_hom_app, coinvariantsTensorIndHom_mk_tmul_indVMk
coinvariantsTensorIndInv 📖	CompOp	3 math math: coinvariantsTensorIndIso_inv, coinvariantsTensorIndNatIso_inv_app, coinvariantsTensorIndInv_mk_tmul_indMk
coinvariantsTensorIndIso 📖	CompOp	2 math math: coinvariantsTensorIndIso_inv, coinvariantsTensorIndIso_hom
coinvariantsTensorIndNatIso 📖	CompOp	2 math math: coinvariantsTensorIndNatIso_inv_app, coinvariantsTensorIndNatIso_hom_app
ind 📖	CompOp	24 math math: coindResAdjunction_counit_app, coindToInd_of_support_subset_orbit, indFunctor_obj, indCoindNatIso_hom_app, indCoindIso_inv_hom_hom, coinvariantsTensorIndIso_inv, indCoindIso_hom_hom_hom, coinvariantsTensorIndIso_hom, coinvariantsTensorIndNatIso_inv_app, coindResAdjunction_unit_app, coindToInd_apply, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, coindResAdjunction_homEquiv_apply, resIndAdjunction_counit_app, coinvariantsTensorIndNatIso_hom_app, indCoindNatIso_inv_app, coindResAdjunction_homEquiv_symm_apply, indMap_hom, resIndAdjunction_unit_app, coinvariantsTensorIndHom_mk_tmul_indVMk, indResHomEquiv_apply_hom, coinvariantsTensorIndInv_mk_tmul_indMk, indResHomEquiv_symm_apply_hom
indFunctor 📖	CompOp	14 math math: coindResAdjunction_counit_app, indFunctor_obj, indCoindNatIso_hom_app, coindResAdjunction_unit_app, indResAdjunction_counit_app_hom_hom, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, resIndAdjunction_counit_app, indCoindNatIso_inv_app, indResAdjunction_unit_app_hom_hom, indFunctor_map, resIndAdjunction_unit_app, instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype, instIsLeftAdjointIndFunctor
indMap 📖	CompOp	2 math math: indFunctor_map, indMap_hom
indResAdjunction 📖	CompOp	4 math math: coindResAdjunction_counit_app, coindResAdjunction_unit_app, indResAdjunction_counit_app_hom_hom, indResAdjunction_unit_app_hom_hom
indResHomEquiv 📖	CompOp	4 math math: coindResAdjunction_homEquiv_apply, coindResAdjunction_homEquiv_symm_apply, indResHomEquiv_apply_hom, indResHomEquiv_symm_apply_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinvariantsTensorIndHom_mk_tmul_indVMk 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor ind Action Action.res ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier coinvariantsTensorIndHom CommSemiring.toSemiring CommRing.toCommSemiring Action.V instAddCommGroupCarrierVModuleCat LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction coinvariantsTensorMk Representation.IndV ρ 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 NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular Representation.Coinvariants.instModule Representation MonoidHom.instFunLike	—	smulCommClass_self RingHomCompTriple.ids Finsupp.sum_single_index zero_smul LinearMap.instSMulCommClass one_smul
coinvariantsTensorIndInv_mk_tmul_indMk 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor Action Action.res ind ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier coinvariantsTensorIndInv CommSemiring.toSemiring CommRing.toCommSemiring TensorProduct Action.V instAddCommGroupCarrierVModuleCat Representation.Coinvariants TensorProduct.addCommGroup TensorProduct.instModule Representation.tprod ρ Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule TensorProduct.tmul LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction coinvariantsTensorMk Representation.IndV Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Finsupp.instAddCommGroup Ring.toAddCommGroup MonoidHom.comp NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
coinvariantsTensorIndIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor ind Action Action.res coinvariantsTensorIndIso coinvariantsTensorIndHom	—	—
coinvariantsTensorIndIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor ind Action Action.res coinvariantsTensorIndIso coinvariantsTensorIndInv	—	—
coinvariantsTensorIndNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor ind CategoryTheory.Functor.comp Action Action.res CategoryTheory.Iso.hom coinvariantsTensorIndNatIso coinvariantsTensorIndHom	—	—
coinvariantsTensorIndNatIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.comp Action Action.res CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor ind CategoryTheory.Iso.inv coinvariantsTensorIndNatIso coinvariantsTensorIndInv	—	—
indFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory indFunctor indMap	—	—
indFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory indFunctor ind	—	—
indMap_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid ind indMap ModuleCat.ofHom Representation.IndV ModuleCat.carrier Action.V ModuleCat.isAddCommGroup ModuleCat.isModule ρ Representation.Coinvariants.instAddCommGroup TensorProduct CommRing.toCommSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module CommSemiring.toSemiring 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 Representation.Coinvariants.instModule Representation.Coinvariants.map LinearMap.lTensor ModuleCat.Hom.hom	—	—
indResAdjunction_counit_app_hom_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of Representation.IndV ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory Action.res ModuleCat.isAddCommGroup ModuleCat.isModule ρ Representation.Coinvariants.instAddCommGroup TensorProduct CommRing.toCommSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module CommSemiring.toSemiring 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 Representation.Coinvariants.instModule Action.Hom.hom indFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Adjunction.counit indResAdjunction Representation.Coinvariants.lift instAddCommGroupCarrierVModuleCat TensorProduct.lift DFunLike.coe AddEquiv LinearMap.addCommMonoid LinearMap.module Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.instAdd EquivLike.toFunLike AddEquiv.instEquivLike Finsupp.lift Representation MonoidHom.instFunLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
indResAdjunction_unit_app_hom_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule Action.Hom.hom ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory Action.res indFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit indResAdjunction Action.V ρ InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
indResHomEquiv_apply_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Action Action.instCategory Action.res DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct ind AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike LinearEquiv.instEquivLike indResHomEquiv ModuleCat.ofHom ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.comp Action.V Ring.toSemiring ModuleCat.Hom.hom ρ InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	RingHomInvPair.ids
indResHomEquiv_symm_apply_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid ind DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action Action.res AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm indResHomEquiv ModuleCat.ofHom Representation.IndV ModuleCat.carrier Action.V ModuleCat.isAddCommGroup ModuleCat.isModule ρ 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 NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular Representation.Coinvariants.instModule Representation.Coinvariants.lift TensorProduct.lift AddEquiv LinearMap.addCommMonoid LinearMap.module Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.instAdd AddEquiv.instEquivLike Finsupp.lift LinearMap.comp instAddCommGroupCarrierVModuleCat Representation MonoidHom.instFunLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid ModuleCat.Hom.hom	—	RingHomInvPair.ids
instIsLeftAdjointIndFunctor 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory indFunctor	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsRightAdjointActionModuleCatRes 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint Action ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.res	—	CategoryTheory.Adjunction.isRightAdjoint

Representation

Definitions

Name	Category	Theorems
IndV 📖	CompOp	10 math math: Rep.coindToInd_of_support_subset_orbit, Rep.indResAdjunction_counit_app_hom_hom, Rep.coindToInd_apply, Rep.indMap_hom, ind_mk, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, ind_apply, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, IndV.hom_ext_iff, Rep.indResHomEquiv_symm_apply_hom
ind 📖	CompOp	2 math math: ind_mk, ind_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ind_apply 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring IndV AddCommGroup.toAddCommMonoid Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule DivInvMonoid.toMonoid Group.toDivInvMonoid TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.instModule tprod MonoidHom.comp NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring leftRegular Coinvariants.instModule MonoidHom.instFunLike ind Coinvariants.map LinearMap.rTensor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.lmapDomain MulOne.toMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
ind_mk 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring IndV AddCommGroup.toAddCommMonoid Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule DivInvMonoid.toMonoid Group.toDivInvMonoid TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.instModule tprod MonoidHom.comp NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring leftRegular Coinvariants.instModule LinearMap.instFunLike Representation MonoidHom.instFunLike ind MulOne.toMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Finsupp.mapDomain_single

Representation.IndV

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	LinearMap.comp Representation.IndV CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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 DivInvMonoid.toMonoid Group.toDivInvMonoid 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 Representation.Coinvariants.instModule RingHomCompTriple.ids	—	—	RingHomCompTriple.ids Representation.Coinvariants.hom_ext TensorProduct.ext Finsupp.lhom_ext' smulCommClass_self LinearMap.ext_ring
hom_ext_iff 📖	mathematical	—	LinearMap.comp Representation.IndV CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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 DivInvMonoid.toMonoid Group.toDivInvMonoid 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 Representation.Coinvariants.instModule RingHomCompTriple.ids	—	RingHomCompTriple.ids hom_ext

---

← Back to Index