Invariants

📁 Source: Mathlib/RepresentationTheory/Invariants.lean

Statistics

Metric	Count
Definitions average, invariantsAdjunction, invariantsFunctor, quotientToInvariants, quotientToInvariantsFunctor, toInvariants, averageMap, invariants, invariantsEquivIntertwiningMap, invariantsEquivFDRepHom, invariantsEquivRepHom, quotientToInvariants, quotientToInvariants_lift, toInvariants	14
Theorems mul_average_left, mul_average_right, instAdditiveModuleCatInvariantsFunctor, instIsRightAdjointModuleCatInvariantsFunctor, instLinearModuleCatInvariantsFunctor, instPreservesZeroMorphismsModuleCatInvariantsFunctor, invariantsAdjunction_counit_app, invariantsAdjunction_homEquiv_apply_hom, invariantsAdjunction_homEquiv_symm_apply_hom, invariantsAdjunction_unit_app, invariantsFunctor_map_hom, invariantsFunctor_obj_carrier, averageMap_id, averageMap_invariant, instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants, invariants_eq_inter, invariants_eq_top, isProj_averageMap, le_comap_invariants, invariantsEquivRepHom_apply, invariantsEquivRepHom_symm_apply_coe, mem_invariants_iff_comm, mem_invariants, mem_invariants_iff_of_forall_mem_zpowers, mem_linHom_invariants_iff_isIntertwining	25
Total	39

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_homEquiv_apply_hom, invariantsAdjunction_counit_app
invariantsFunctor 📖	CompOp	12 math math: invariantsAdjunction_homEquiv_symm_apply_hom, invariantsFunctor_obj_carrier, instIsRightAdjointModuleCatInvariantsFunctor, invariantsAdjunction_unit_app, instPreservesZeroMorphismsModuleCatInvariantsFunctor, groupCohomology.map_id_comp_H0Iso_hom, instLinearModuleCatInvariantsFunctor, invariantsAdjunction_homEquiv_apply_hom, invariantsFunctor_map_hom, invariantsAdjunction_counit_app, instAdditiveModuleCatInvariantsFunctor, groupCohomology.map_id_comp_H0Iso_hom_assoc
quotientToInvariants 📖	CompOp	2 math math: groupCohomology.H1InfRes_X₁, groupCohomology.H1InfRes_f
quotientToInvariantsFunctor 📖	CompOp	1 math math: groupCohomology.infNatTrans_app
toInvariants 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveModuleCatInvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat CommRing.toRing instCategory ModuleCat.moduleCategory instPreadditive ModuleCat.instPreadditive invariantsFunctor	—	—
instIsRightAdjointModuleCatInvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint ModuleCat CommRing.toRing ModuleCat.moduleCategory Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory invariantsFunctor	—	CategoryTheory.Adjunction.isRightAdjoint
instLinearModuleCatInvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring Rep DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat CommRing.toRing instCategory ModuleCat.moduleCategory instPreadditive ModuleCat.instPreadditive instLinear ModuleCat.instLinear invariantsFunctor	—	—
instPreservesZeroMorphismsModuleCatInvariantsFunctor 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive ModuleCat.instPreadditive invariantsFunctor	—	—
invariantsAdjunction_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep Ring.toSemiring CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Functor.comp ModuleCat ModuleCat.moduleCategory invariantsFunctor trivialFunctor CategoryTheory.Functor.id CategoryTheory.Adjunction.counit invariantsAdjunction ofHom ModuleCat.carrier CategoryTheory.Functor.obj V ModuleCat.isAddCommGroup hV1 ModuleCat.isModule hV2 Representation.trivial AddCommGroup.toAddCommMonoid ρ Submodule.subtype CommSemiring.toSemiring CommRing.toCommSemiring Representation.invariants	—	—
invariantsAdjunction_homEquiv_apply_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing CategoryTheory.Functor.obj Rep Ring.toSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid 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 V AddCommGroup.toAddCommMonoid hV1 hV2 RingHom.id Semiring.toNonAssocSemiring Representation.invariants CommSemiring.toSemiring CommRing.toCommSemiring ρ Representation.IntertwiningMap.toLinearMap Hom.hom	—	—
invariantsAdjunction_homEquiv_symm_apply_hom 📖	mathematical	—	Representation.IntertwiningMap.toLinearMap V Ring.toSemiring CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory Rep instCategory trivialFunctor AddCommGroup.toAddCommMonoid hV1 hV2 ρ 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 CommSemiring.toSemiring CommRing.toCommSemiring Submodule SetLike.instMembership Submodule.setLike Representation.invariants ModuleCat.isAddCommGroup Submodule.addCommMonoid ModuleCat.isModule Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Submodule.subtype ModuleCat.Hom.hom	—	—
invariantsAdjunction_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp Rep Ring.toSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory trivialFunctor invariantsFunctor CategoryTheory.Adjunction.unit invariantsAdjunction ModuleCat.ofHom ModuleCat.carrier V CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.obj Submodule AddCommGroup.toAddCommMonoid hV1 hV2 SetLike.instMembership Submodule.setLike Representation.invariants ρ ModuleCat.isAddCommGroup ModuleCat.isModule Submodule.addCommGroup Submodule.module LinearMap.codRestrict RingHom.id Semiring.toNonAssocSemiring LinearMap.id	—	—
invariantsFunctor_map_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of V CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule AddCommGroup.toAddCommMonoid hV1 hV2 SetLike.instMembership Submodule.setLike Representation.invariants ρ Submodule.addCommGroup Submodule.module CategoryTheory.Functor.map Rep instCategory ModuleCat ModuleCat.moduleCategory invariantsFunctor LinearMap.codRestrict Submodule.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.comp Representation.IntertwiningMap.toLinearMap Hom.hom Submodule.subtype	—	—
invariantsFunctor_obj_carrier 📖	mathematical	—	ModuleCat.carrier CommRing.toRing CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory ModuleCat ModuleCat.moduleCategory invariantsFunctor V	—	—

Representation

Definitions

Name	Category	Theorems
averageMap 📖	CompOp	3 math math: isProj_averageMap, averageMap_invariant, averageMap_id
invariants 📖	CompOp	44 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, card_inv_mul_sum_char_eq_finrank, instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, groupCohomology.shortComplexH0_f, isProj_averageMap, 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, linHom.invariantsEquivRepHom_apply, 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, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, le_comap_invariants, invariants_eq_inter, groupCohomology.δ₀_apply, Rep.invariantsAdjunction_homEquiv_apply_hom, Rep.invariantsFunctor_map_hom, Rep.invariantsAdjunction_counit_app, 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, invariants_eq_top, groupCohomology.map_id_comp_H0Iso_hom_assoc
invariantsEquivIntertwiningMap 📖	CompOp	—
quotientToInvariants 📖	CompOp	—
quotientToInvariants_lift 📖	CompOp	2 math math: groupCohomology.infNatTrans_app, groupCohomology.H1InfRes_f
toInvariants 📖	CompOp	1 math math: instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
averageMap_id 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike invariants	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid 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 CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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 CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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 AddCommGroup.toAddCommMonoid AddSubmonoid.toAddSubsemigroup Submodule.toAddSubmonoid CommSemiring.toSemiring CommRing.toCommSemiring 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 CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instTop	—	eq_top_iff isTrivial_apply
isProj_averageMap 📖	mathematical	—	LinearMap.IsProj CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid invariants LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike averageMap	—	averageMap_invariant averageMap_id
le_comap_invariants 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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 CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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 CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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	—	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
mem_linHom_invariants_iff_isIntertwining 📖	mathematical	—	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe Representation DivInvMonoid.toMonoid Group.toDivInvMonoid LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid IsIntertwiningMap	—	RingHomCompTriple.ids inv_self_apply LinearMap.ext IsIntertwiningMap.isIntertwining self_inv_apply

Representation.linHom

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invariantsEquivRepHom_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Rep.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Submodule LinearMap.addCommGroup 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 Rep.instCategory Submodule.addCommMonoid Rep.instAddCommGroupHom Submodule.module Rep.instModuleHom EquivLike.toFunLike LinearEquiv.instEquivLike invariantsEquivRepHom Rep.ofHom	—	RingHomInvPair.ids smulCommClass_self
invariantsEquivRepHom_symm_apply_coe 📖	mathematical	—	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Rep.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 Submodule LinearMap.addCommGroup 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 Rep.instCategory smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Rep.instAddCommGroupHom Submodule.addCommMonoid Rep.instModuleHom Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm invariantsEquivRepHom SemilinearMapClass.semilinearMap Representation.IntertwiningMap Rep.Hom.hom Representation.IntertwiningMap.instFunLike	—	RingHomInvPair.ids smulCommClass_self
mem_invariants_iff_comm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Rep.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.hV1 Rep.hV2 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 Rep.ρ_mul inv_mul_cancel map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass Module.End.one_eq_id LinearMap.comp_id mul_inv_cancel

---

← Back to Index