Invariants

📁 Source: Mathlib/RepresentationTheory/Invariants.lean

Statistics

Metric	Count
Definitions average, invariantsAdjunction, invariantsFunctor, quotientToInvariants, quotientToInvariantsFunctor, toInvariants, averageMap, invariants, invariantsEquivFDRepHom, invariantsEquivRepHom, quotientToInvariants, toInvariants	12
Theorems mul_average_left, mul_average_right, instAdditiveModuleCatInvariantsFunctor, instIsRightAdjointModuleCatInvariantsFunctor, instLinearModuleCatInvariantsFunctor, instPreservesZeroMorphismsModuleCatInvariantsFunctor, invariantsAdjunction_counit_app_hom, invariantsAdjunction_homEquiv_apply_hom, invariantsAdjunction_homEquiv_symm_apply_hom, invariantsAdjunction_unit_app, invariantsFunctor_map_hom, invariantsFunctor_obj_carrier, quotientToInvariantsFunctor_map_hom, quotientToInvariantsFunctor_obj_V, averageMap_id, averageMap_invariant, instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants, invariants_eq_inter, invariants_eq_top, isProj_averageMap, le_comap_invariants, invariantsEquivRepHom_apply_hom, invariantsEquivRepHom_symm_apply_coe, mem_invariants_iff_comm, mem_invariants, mem_invariants_iff_of_forall_mem_zpowers	26
Total	38

GroupAlgebra

Definitions

Name	Category	Theorems
average 📖	CompOp	2 math math: mul_average_left, mul_average_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_average_left 📖	mathematical	—	MonoidAlgebra CommSemiring.toSemiring MonoidAlgebra.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne average	—	Finset.sum_congr Algebra.mul_smul_comm Finset.mul_sum MonoidAlgebra.single_mul_single mul_one Function.Bijective.sum_comp Group.mulLeft_bijective
mul_average_right 📖	mathematical	—	MonoidAlgebra CommSemiring.toSemiring MonoidAlgebra.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid average Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Finset.sum_congr Algebra.smul_mul_assoc Finset.sum_mul MonoidAlgebra.single_mul_single mul_one Function.Bijective.sum_comp Group.mulRight_bijective

Rep

Definitions

Name	Category	Theorems
invariantsAdjunction 📖	CompOp	4 math math: invariantsAdjunction_homEquiv_symm_apply_hom, invariantsAdjunction_unit_app, invariantsAdjunction_counit_app_hom, invariantsAdjunction_homEquiv_apply_hom
invariantsFunctor 📖	CompOp	13 math math: invariantsAdjunction_homEquiv_symm_apply_hom, invariantsFunctor_obj_carrier, instIsRightAdjointModuleCatInvariantsFunctor, invariantsAdjunction_unit_app, instPreservesZeroMorphismsModuleCatInvariantsFunctor, quotientToInvariantsFunctor_map_hom, groupCohomology.map_id_comp_H0Iso_hom, invariantsAdjunction_counit_app_hom, instLinearModuleCatInvariantsFunctor, invariantsAdjunction_homEquiv_apply_hom, invariantsFunctor_map_hom, instAdditiveModuleCatInvariantsFunctor, groupCohomology.map_id_comp_H0Iso_hom_assoc
quotientToInvariants 📖	CompOp	3 math math: quotientToInvariantsFunctor_map_hom, groupCohomology.H1InfRes_X₁, groupCohomology.H1InfRes_f
quotientToInvariantsFunctor 📖	CompOp	3 math math: groupCohomology.infNatTrans_app, quotientToInvariantsFunctor_map_hom, quotientToInvariantsFunctor_obj_V
toInvariants 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveModuleCatInvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat Action.instCategory ModuleCat.moduleCategory Action.instPreadditive ModuleCat.instPreadditive invariantsFunctor	—	—
instIsRightAdjointModuleCatInvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint ModuleCat CommRing.toRing ModuleCat.moduleCategory Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory invariantsFunctor	—	CategoryTheory.Adjunction.isRightAdjoint
instLinearModuleCatInvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat Action.instCategory ModuleCat.moduleCategory Action.instPreadditive ModuleCat.instPreadditive instLinearRep ModuleCat.instLinear invariantsFunctor	—	—
instPreservesZeroMorphismsModuleCatInvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms Rep CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory Action.instHasZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive invariantsFunctor	—	—
invariantsAdjunction_counit_app_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory CategoryTheory.Functor.comp invariantsFunctor trivialFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit invariantsAdjunction ModuleCat.ofHom ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule Submodule.subtype Action.V Ring.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Representation.invariants CommRing.toCommSemiring ρ	—	—
invariantsAdjunction_homEquiv_apply_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing CategoryTheory.Functor.obj Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory invariantsFunctor DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct trivialFunctor EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv invariantsAdjunction LinearMap.codRestrict ModuleCat.carrier Action.V Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring Representation.invariants CommRing.toCommSemiring instAddCommGroupCarrierVModuleCat ρ Action.Hom.hom	—	—
invariantsAdjunction_homEquiv_symm_apply_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Rep Action.instCategory trivialFunctor Action.Hom.hom DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct invariantsFunctor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv invariantsAdjunction LinearMap.comp ModuleCat.carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants CommRing.toCommSemiring ρ ModuleCat.isAddCommGroup Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Submodule.subtype	—	—
invariantsAdjunction_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory trivialFunctor invariantsFunctor CategoryTheory.Adjunction.unit invariantsAdjunction ModuleCat.ofHom ModuleCat.carrier Action.V CategoryTheory.Functor.obj Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants ρ ModuleCat.isAddCommGroup Submodule.addCommGroup Submodule.module LinearMap.codRestrict Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.id	—	—
invariantsFunctor_map_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module CategoryTheory.Functor.map Rep Action.instCategory invariantsFunctor LinearMap.codRestrict Ring.toSemiring Submodule.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.comp Action.Hom.hom Submodule.subtype	—	—
invariantsFunctor_obj_carrier 📖	mathematical	—	ModuleCat.carrier CommRing.toRing CategoryTheory.Functor.obj Rep DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory invariantsFunctor Action.V	—	—
quotientToInvariantsFunctor_map_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group quotientToInvariants CategoryTheory.Functor.map Rep Action.instCategory quotientToInvariantsFunctor SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup invariantsFunctor CategoryTheory.Functor.obj Action Action.res Subgroup.subtype	—	—
quotientToInvariantsFunctor_obj_V 📖	mathematical	—	Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group CategoryTheory.Functor.obj Rep Action.instCategory quotientToInvariantsFunctor ModuleCat.of ModuleCat.carrier Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Subgroup.instSetLike Subgroup.toGroup MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ Subgroup.subtype Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module	—	—

Representation

Definitions

Name	Category	Theorems
averageMap 📖	CompOp	3 math math: isProj_averageMap, averageMap_invariant, averageMap_id
invariants 📖	CompOp	45 math math: Rep.invariantsAdjunction_homEquiv_symm_apply_hom, groupCohomology.cocyclesIso₀_hom_comp_f, groupCohomology.π_comp_H0Iso_hom, groupCohomology.H0IsoOfIsTrivial_hom, groupCohomology.map_H0Iso_hom_f_apply, groupCohomology.H0IsoOfIsTrivial_inv_apply, instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, groupCohomology.shortComplexH0_f, isProj_averageMap, groupCohomology.infNatTrans_app, Rep.invariantsAdjunction_unit_app, groupCohomology.subtype_comp_d₀₁_apply, mem_invariants_iff_of_forall_mem_zpowers, groupCohomology.map_H0Iso_hom_f, mem_invariants, FDRep.average_char_eq_finrank_invariants, groupCohomology.π_comp_H0Iso_hom_apply, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupCohomology.π_comp_H0Iso_hom_assoc, groupCohomology.d₀₁_ker_eq_invariants, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, averageMap_invariant, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.subtype_comp_d₀₁_assoc, groupCohomology.map_id_comp_H0Iso_hom, linHom.invariantsEquivRepHom_symm_apply_coe, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, Rep.invariantsAdjunction_counit_app_hom, Rep.quotientToInvariantsFunctor_obj_V, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, le_comap_invariants, invariants_eq_inter, Rep.invariantsAdjunction_homEquiv_apply_hom, Rep.invariantsFunctor_map_hom, groupCohomology.cocyclesIso₀_hom_comp_f_apply, groupCohomology.subtype_comp_d₀₁, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, groupCohomology.cocyclesMk₀_eq, groupCohomology.map_H0Iso_hom_f_assoc, linHom.invariantsEquivRepHom_apply_hom, groupCohomology.H1InfRes_f, invariants_eq_top, groupCohomology.map_id_comp_H0Iso_hom_assoc
quotientToInvariants 📖	CompOp	—
toInvariants 📖	CompOp	1 math math: instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
averageMap_id 📖	mathematical	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike invariants	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike averageMap	—	smulCommClass_self Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass IsScalarTower.left asAlgebraHom_single one_smul LinearMap.coe_sum Finset.sum_apply mem_invariants Finset.sum_const Nat.cast_smul_eq_nsmul smul_smul invOf_mul_self'
averageMap_invariant 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike invariants DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike averageMap	—	averageMap.eq_1 smulCommClass_self IsScalarTower.left asAlgebraHom_single_one Module.End.mul_apply map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass GroupAlgebra.mul_average_left
instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants 📖	mathematical	—	IsTrivial Subgroup SetLike.instMembership Subgroup.instSetLike Submodule CommSemiring.toSemiring Submodule.setLike invariants Subgroup.toGroup MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Subgroup.subtype Submodule.addCommMonoid Submodule.module toInvariants	—	LinearMap.ext
invariants_eq_inter 📖	mathematical	—	AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.toAddSubsemigroup Submodule.toAddSubmonoid CommSemiring.toSemiring invariants Set.iInter Function.fixedPoints DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	Set.ext
invariants_eq_top 📖	mathematical	—	invariants Top.top Submodule CommSemiring.toSemiring Submodule.instTop	—	eq_top_iff isTrivial_apply
isProj_averageMap 📖	mathematical	—	LinearMap.IsProj CommSemiring.toSemiring invariants LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike averageMap	—	averageMap_invariant averageMap_id
le_comap_invariants 📖	mathematical	—	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder invariants Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Subgroup.subtype Submodule.comap DFunLike.coe Representation MonoidHom.instFunLike	—	Subgroup.Normal.conj_mem' map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass self_inv_apply
mem_invariants 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike invariants DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	—
mem_invariants_iff_of_forall_mem_zpowers 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers	Submodule CommSemiring.toSemiring Submodule.setLike invariants DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	Int.induction_on zpow_zero map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass zpow_add_one zpow_natCast map_mul MonoidHomClass.toMulHomClass map_pow neg_sub_comm zpow_sub zpow_neg zpow_one inv_self_apply

Representation.linHom

Definitions

Name	Category	Theorems
invariantsEquivFDRepHom 📖	CompOp	—
invariantsEquivRepHom 📖	CompOp	2 math math: invariantsEquivRepHom_symm_apply_coe, invariantsEquivRepHom_apply_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invariantsEquivRepHom_apply_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap ModuleCat.carrier Action.V AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule Submodule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.instMembership Submodule.setLike Representation.invariants Representation.linHom Rep.ρ Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory Submodule.addCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Submodule.module CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike LinearEquiv.instEquivLike invariantsEquivRepHom ModuleCat.ofHom ModuleCat.isAddCommGroup	—	RingHomInvPair.ids smulCommClass_self
invariantsEquivRepHom_symm_apply_coe 📖	mathematical	—	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule Submodule LinearMap.addCommMonoid LinearMap.module SetLike.instMembership Submodule.setLike Representation.invariants Representation.linHom Rep.ρ DFunLike.coe LinearEquiv RingHomInvPair.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Submodule.addCommMonoid CategoryTheory.Linear.homModule instLinearRep Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm invariantsEquivRepHom ModuleCat.Hom.hom Action.Hom.hom	—	RingHomInvPair.ids smulCommClass_self
mem_invariants_iff_comm 📖	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 AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.linHom Rep.ρ LinearMap.comp RingHomCompTriple.ids	—	smulCommClass_self RingHomCompTriple.ids LinearMap.comp_assoc ModuleCat.hom_ofHom ModuleCat.hom_comp Rep.ofHom_ρ Action.ρAut_apply_inv Action.ρAut_apply_hom ModuleCat.hom_ext_iff CategoryTheory.Iso.inv_comp_eq comm IsEquiv.toSymm eq_isEquiv

---

← Back to Index