Intertwining

📁 Source: Mathlib/RepresentationTheory/Intertwining.lean

Statistics

Metric	Count
Definitions `intertwiningMap_of_isIntertwiningMap`, `dualTensorHom`, `instEquivLike`, `invFun`, `mk`, `refl`, `toIntertwiningMap`, `toLinearEquiv`, `trans`, `IntertwiningMap`, `centralMul`, `coeFnAddMonoidHom`, `comp`, `equivAlgEnd`, `equivLinearMapAsModule`, `id`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instAlgebra`, `instFunLike`, `instModule`, `instMonoid`, `instMul`, `instNatCast`, `instNeg`, `instOne`, `instPowNat`, `instSMul`, `instSMulInt`, `instSMulNat`, `instSemigroup`, `instSemiring`, `instSub`, `instZero`, `ker`, `lTensor`, `llcomp`, `ofBijective`, `rTensor`, `range`, `tensor`, `toLinearMap`, `toLinearMapl`, `IsIntertwiningMap`, `assoc`, `comm`, `lid`, `rid`	49
Theorems `isIntertwining_symm_isIntertwining`, `toIntertwiningMap`, `apply_symm_apply`, `coe_invFun`, `coe_symm`, `coe_toIntertwiningMap`, `coe_toLinearMap`, `conj_apply_self`, `dualTensorHom_invFun`, `dualTensorHom_toFun`, `ext`, `ext_iff`, `instLinearEquivClass`, `left_inv`, `mk_apply`, `mk_symm`, `refl_apply`, `right_inv`, `symm_apply_apply`, `symm_trans`, `toIntertwiningMap_mk'`, `toIntertwiningMap_refl`, `toIntertwiningMap_trans`, `toLinearEquiv_apply`, `toLinearEquiv_inj`, `toLinearEquiv_injective`, `toLinearEquiv_mk'`, `toLinearEquiv_toLinearMap`, `toLinearMap_mk'`, `toLinearMap_refl`, `toLinearMap_symm`, `toLinearMap_trans`, `trans_apply`, `trans_symm`, `add_comp`, `add_toLinearMap`, `algebraMap_apply`, `coe_add`, `coe_eq_toLinearMap`, `coe_mk`, `coe_mul`, `coe_neg`, `coe_nsmul`, `coe_ofBijective`, `coe_one`, `coe_smul`, `coe_sub`, `coe_toLinearMap`, `coe_zero`, `coe_zsmul`, `comp_add`, `comp_apply`, `comp_def`, `comp_smul`, `comp_toLinearMap`, `ext`, `ext_iff`, `id_apply`, `instFiniteOfIsNoetherian`, `instLinearMapClass`, `isIntertwining`, `isIntertwining'`, `isIntertwiningMap_of_mem_center`, `isIntertwining_assoc`, `ker_toSubmodule`, `lTensor_add`, `lTensor_apply`, `lTensor_comp_rTensor`, `lTensor_id`, `lTensor_smul`, `lTensor_zero`, `mem_ker`, `mem_range`, `mul_apply`, `rTensor_add`, `rTensor_apply`, `rTensor_comp_lTensor`, `rTensor_id`, `rTensor_smul`, `rTensor_zero`, `range_toSubmodule`, `smul_apply`, `smul_comp`, `sub_toLinearMap`, `sum_apply`, `tensor_add_left`, `tensor_add_right`, `tensor_apply`, `tensor_smul_left`, `tensor_smul_right`, `toFun_injective`, `toLinearMap_apply`, `toLinearMap_id`, `toLinearMap_injective`, `toLinearMap_lTensor`, `toLinearMap_mk`, `toLinearMap_rTensor`, `toLinearMap_smul`, `toLinearMap_sum`, `toLinearMap_tensor`, `toLinearMapl_apply`, `zero_toLinearMap`, `isIntertwining`, `assoc_apply`, `assoc_symm_toLinearMap`, `comm_apply`, `comm_comp_lTensor`, `comm_comp_rTensor`, `comm_symm`, `lid_apply`, `lid_symm_apply`, `rid_apply`, `rid_symm_apply`, `toLinearMap_assoc`, `toLinearMap_comm`, `toLinearMap_lid`, `toLinearMap_rid`, `isIntertwiningMap_iff`	118
Total	167

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntertwining_symm_isIntertwining` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `toLinearMap` `RingHomInvPair.ids` `DFunLike.coe` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `toLinearMap` `RingHomInvPair.ids` `symm` `DFunLike.coe` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `comp_toLinearMap_eq_iff` `LinearMap.comp_assoc` `RingHomInvPair.triples₂` `comp_symm` `RingHomCompTriple.right_ids` `LinearMap.id_comp` `LinearMap.comp_id`

LinearMap

Definitions

Name	Category	Theorems
`intertwiningMap_of_isIntertwiningMap` 📖	CompOp	1 math math: `toIntertwiningMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIntertwiningMap` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `Representation` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	`DFunLike.coe` `Representation.IntertwiningMap` `Representation.IntertwiningMap.instFunLike` `intertwiningMap_of_isIntertwiningMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	—	—

Representation

Definitions

Name	Category	Theorems
`IntertwiningMap` 📖	CompData	185 math math: `groupHomology.mapCycles₂_comp_assoc`, `IntertwiningMap.comp_add`, `IntertwiningMap.rTensor_zero`, `IntertwiningMap.mul_apply`, `groupHomology.coinvariantsMk_comp_H0Iso_inv_apply`, `Rep.ofHom_sub`, `groupHomology.chainsMap_f_3_comp_chainsIso₃_apply`, `Rep.resCoindToHom_hom_apply_coe`, `groupHomology.mapCycles₁_comp_apply`, `freeLift_single_single`, `IntertwiningMap.instLinearMapClass`, `Equiv.coe_toIntertwiningMap`, `IntertwiningMap.toLinearMap_injective`, `groupHomology.mapCycles₁_comp_assoc`, `Rep.add_hom`, `IntertwiningMap.coe_mul`, `Rep.preservesLimits_forget`, `Rep.hom_surjective`, `Rep.hom_bijective`, `groupHomology.π_comp_H0Iso_hom_assoc`, `LinearizeMonoidal.μ_apply_single_single`, `groupCohomology.mapShortComplexH2_comp_assoc`, `IntertwiningMap.coe_toLinearMap`, `Rep.norm_comm_apply`, `IntertwiningMap.comp_apply`, `card_inv_mul_sum_char_mul_char_eq_finrank`, `IntertwiningMap.coe_zero`, `IntertwiningMap.coe_zsmul`, `IntertwiningMap.lTensor_add`, `FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ`, `equivOfIso_toFun`, `Rep.standardComplex.εToSingle₀_comp_eq`, `IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed`, `IntertwiningMap.tensor_add_left`, `Rep.instEpiModuleCatAppCoinvariantsMk`, `Rep.ofHom_add`, `IntertwiningMap.sub_toLinearMap`, `Rep.forget_map`, `groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc`, `groupHomology.cyclesMap_comp_assoc`, `IntertwiningMap.toLinearMap_sum`, `groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply`, `Rep.applyAsHom_comm_apply`, `groupHomology.chainsMap_f_single`, `Rep.coindFunctorIso_inv_app_hom_toFun_coe`, `Rep.instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier`, `groupHomology.coinvariantsMk_comp_H0Iso_inv`, `IntertwiningMap.tensor_smul_right`, `Rep.indToCoindAux_comm`, `groupHomology.map_comp_assoc`, `IsIrreducible.bijective_or_eq_zero`, `Rep.forget_obj`, `LinearizeMonoidal.ε_one`, `IntertwiningMap.smul_apply`, `IntertwiningMap.sum_apply`, `groupCohomology.cochainsMap_comp_assoc`, `groupHomology.pOpcycles_comp_opcyclesIso_hom_apply`, `groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply`, `Rep.subtype_hom_toFun`, `Rep.coinvariantsFunctor_hom_ext_iff`, `IntertwiningMap.algebraMap_apply`, `Equiv.toLinearEquiv_apply`, `IntertwiningMap.lTensor_zero`, `Rep.smul_hom`, `Rep.mkIso_hom_hom_apply`, `groupCohomology.norm_ofAlgebraAutOnUnits_eq`, `groupHomology.d₁₀_comp_coinvariantsMk`, `groupHomology.mapCycles₂_comp_apply`, `Rep.hom_injective`, `IntertwiningMap.toLinearMap_smul`, `Rep.zsmul_hom`, `IsIrreducible.finrank_intertwiningMap_self`, `IsIrreducible.injective_or_eq_zero`, `Rep.inv_hom_apply`, `Rep.nsmul_hom`, `Rep.mkIso_inv_hom_apply`, `groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply`, `IsIrreducible.instSubsingletonIntertwiningMapOfIsEmptyEquiv`, `IntertwiningMap.comp_def`, `IntertwiningMap.tensor_add_right`, `coindMap_coe_apply_apply`, `Rep.zero_hom`, `Rep.preservesColimits_forget`, `Rep.ofHom_nsmul`, `LinearizeMonoidal.η_single`, `IntertwiningMap.toLinearMap_apply`, `linHom.invariantsEquivRepHom_symm_apply_coe`, `IntertwiningMap.coe_eq_toLinearMap`, `groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply`, `IntertwiningMap.rTensor_smul`, `IntertwiningMap.toFun_injective`, `equivOfIso_invFun`, `IntertwiningMap.id_apply`, `Rep.sub_hom`, `IntertwiningMap.mem_ker`, `Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun`, `Rep.standardComplex.quasiIso_forget₂_εToSingle₀`, `Rep.leftRegularHom_hom_single`, `Rep.homEquiv_apply`, `Rep.coinvariantsAdjunction_unit_app`, `Rep.coinvariantsMk_app_hom`, `Rep.forget₂_moduleCat_obj`, `groupCohomology.cocyclesMap_comp_assoc`, `IntertwiningMap.add_comp`, `groupHomology.pOpcycles_comp_opcyclesIso_hom`, `IntertwiningMap.coe_add`, `IntertwiningMap.tensor_smul_left`, `groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv`, `Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier`, `IntertwiningMap.coe_sub`, `FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ`, `IntertwiningMap.lTensor_apply`, `Rep.leftRegularHomEquiv_symm_single`, `Rep.forget₂_moduleCat_map`, `LinearizeMonoidal.δ_apply_single`, `groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc`, `Rep.instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier`, `Rep.norm_apply`, `linearizeMap_single`, `Rep.hom_comm_apply`, `Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply`, `Rep.sum_hom`, `Rep.standardComplex.d_apply`, `groupHomology.π_comp_H0Iso_hom`, `Rep.homEquiv_symm_apply`, `groupCohomology.mapShortComplexH1_comp_assoc`, `groupHomology.H0π_comp_H0Iso_hom`, `FDRep.forget₂_ρ`, `Rep.id_apply`, `Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq`, `IntertwiningMap.mem_range`, `IntertwiningMap.lTensor_smul`, `IntertwiningMap.rTensor_add`, `Rep.ofHom_sum`, `Rep.comp_apply`, `IntertwiningMap.isIntertwining`, `IntertwiningMap.coe_ofBijective`, `IntertwiningMap.instFiniteOfIsNoetherian`, `IntertwiningMap.coe_neg`, `IntertwiningMap.zero_toLinearMap`, `groupHomology.shortComplexH0_g`, `Rep.applyAsHom_apply`, `Rep.mkQ_hom_toFun`, `leftRegularMapEquiv_symm_single`, `Rep.epi_iff_surjective`, `groupHomology.d₁₀_comp_coinvariantsMk_assoc`, `IntertwiningMap.comp_smul`, `groupHomology.chainsMap_f_0_comp_chainsIso₀_apply`, `groupHomology.H0π_comp_H0Iso_hom_assoc`, `Rep.ofHom_zsmul`, `coindMap_coe_apply`, `IntertwiningMap.coe_mk`, `freeLiftLEquiv_symm_apply`, `FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing`, `Rep.hom_inv_apply`, `LinearizeMonoidal.μ_apply_apply`, `Rep.coinvariantsAdjunction_homEquiv_apply_hom`, `leftRegularMapEquiv_apply`, `IntertwiningMap.coe_nsmul`, `IntertwiningMap.add_toLinearMap`, `freeLiftLEquiv_apply`, `FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ`, `Rep.ofHom_apply`, `IntertwiningMap.coe_smul`, `Rep.reflectsIsomorphisms_forget`, `groupHomology.H0π_comp_H0Iso_hom_apply`, `Rep.barComplex.d_single`, `Rep.mono_iff_injective`, `LinearMap.toIntertwiningMap`, `groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc`, `groupHomology.chainsMap_f_1_comp_chainsIso₁_apply`, `IntertwiningMap.toLinearMapl_apply`, `Rep.ofHom_zero`, `groupHomology.H0π_comp_map_apply`, `IntertwiningMap.rTensor_apply`, `IntertwiningMap.smul_comp`, `Rep.ofHom_smul`, `Rep.ofHom_neg`, `IntertwiningMap.tensor_apply`, `Rep.neg_hom`, `leftRegularMapEquiv_symm_apply_toFun`, `groupHomology.chainsMap_f_2_comp_chainsIso₂_apply`, `IntertwiningMap.coe_one`, `groupCohomology.map_comp_assoc`, `Rep.coindFunctorIso_hom_app_hom_toFun_hom_toFun`
`IsIntertwiningMap` 📖	CompData	3 math math: `IntertwiningMap.isIntertwiningMap_of_mem_center`, `isIntertwiningMap_iff`, `mem_linHom_invariants_iff_isIntertwining`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntertwiningMap_iff` 📖	mathematical	—	`IsIntertwiningMap` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Representation` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	—

Representation.Equiv

Definitions

Name	Category	Theorems
`dualTensorHom` 📖	CompOp	2 math math: `dualTensorHom_toFun`, `dualTensorHom_invFun`
`instEquivLike` 📖	CompOp	34 math math: `mk_apply`, `Representation.finsuppTensorLeft_apply_tmul`, `coe_toIntertwiningMap`, `instLinearEquivClass`, `Representation.finsuppTensorRight_apply_tmul`, `Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single`, `Representation.equivOfIso_toFun`, `apply_symm_apply`, `Representation.TensorProduct.rid_symm_apply`, `Representation.linearizeTrivialIso_apply`, `trans_apply`, `Rep.mkIso_inv_hom_apply`, `Representation.linearizeOfMulActionIso_apply`, `Representation.TensorProduct.rid_apply`, `Representation.finsuppTensorRight_symm_apply_single`, `Representation.TensorProduct.comm_apply`, `Representation.finsuppTensorLeft_symm_apply_single`, `dualTensorHom_toFun`, `Representation.leftRegularTensorTrivialIsoFree_apply_single_tmul_single`, `Representation.linearizeOfMulActionIso_symm_apply`, `symm_apply_apply`, `ext_iff`, `coe_symm`, `Representation.TensorProduct.lid_symm_apply`, `Representation.diagonalOneEquivLeftRegular_symm_apply_single`, `Representation.finsuppTensorLeft_apply_tmul_apply`, `Representation.IntertwiningMap.coe_ofBijective`, `Representation.TensorProduct.assoc_apply`, `refl_apply`, `Representation.diagonalOneEquivLeftRegular_apply_single`, `Representation.TensorProduct.lid_apply`, `Representation.finsuppTensorRight_apply_tmul_apply`, `coe_toLinearMap`, `Representation.linearizeTrivialIso_symm_apply`
`invFun` 📖	CompOp	5 math math: `right_inv`, `Representation.equivOfIso_invFun`, `left_inv`, `dualTensorHom_invFun`, `coe_invFun`
`mk` 📖	CompOp	—
`refl` 📖	CompOp	5 math math: `toLinearMap_refl`, `trans_symm`, `toIntertwiningMap_refl`, `symm_trans`, `refl_apply`
`toIntertwiningMap` 📖	CompOp	39 math math: `Rep.hom_hom_associator`, `toLinearMap_refl`, `coe_toIntertwiningMap`, `toLinearEquiv_toLinearMap`, `toIntertwiningMap_trans`, `Representation.ofMulActionSubsingletonEquivTrivial_symm_apply`, `Representation.TensorProduct.assoc_symm_toLinearMap`, `Rep.hom_hom_leftUnitor`, `Representation.LinearizeMonoidal.μ_comp_assoc`, `Representation.ofMulActionSubsingletonEquivTrivial_apply`, `toLinearEquiv_apply`, `toIntertwiningMap_refl`, `Rep.mkIso_hom_hom_apply`, `Rep.hom_braiding`, `right_inv`, `Representation.LinearizeMonoidal.assoc_comp_δ`, `Representation.TensorProduct.comm_comp_rTensor`, `toLinearMap_mk'`, `Representation.LinearizeMonoidal.rightUnitor_δ`, `Rep.hom_inv_rightUnitor`, `Rep.hom_hom_rightUnitor`, `Rep.mkIso_inv_hom_toLinearMap`, `toIntertwiningMap_mk'`, `left_inv`, `Representation.TensorProduct.toLinearMap_assoc`, `Representation.LinearizeMonoidal.leftUnitor_δ`, `Representation.TensorProduct.comm_comp_lTensor`, `Rep.mkIso_hom_hom`, `Representation.LinearizeMonoidal.μ_leftUnitor`, `Rep.hom_inv_leftUnitor`, `Rep.hom_inv_associator`, `Representation.LinearizeMonoidal.μ_rightUnitor`, `toLinearMap_symm`, `Representation.TensorProduct.toLinearMap_rid`, `toLinearMap_trans`, `Rep.mkIso_hom_hom_toLinearMap`, `Representation.TensorProduct.toLinearMap_comm`, `coe_toLinearMap`, `Representation.TensorProduct.toLinearMap_lid`
`toLinearEquiv` 📖	CompOp	10 math math: `toLinearEquiv_mk'`, `toLinearEquiv_toLinearMap`, `toLinearEquiv_apply`, `toLinearEquiv_injective`, `Rep.indCoindIso_inv_hom_toLinearMap`, `coe_symm`, `toLinearMap_symm`, `coe_invFun`, `conj_apply_self`, `toLinearEquiv_inj`
`trans` 📖	CompOp	5 math math: `trans_symm`, `toIntertwiningMap_trans`, `trans_apply`, `symm_trans`, `toLinearMap_trans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`right_inv`
`coe_invFun` 📖	mathematical	—	`invFun` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `toLinearEquiv`	—	—
`coe_symm` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `toLinearEquiv` `Representation.Equiv` `instEquivLike` `symm`	—	`RingHomInvPair.ids`
`coe_toIntertwiningMap` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `Representation.IntertwiningMap.instFunLike` `toIntertwiningMap` `Representation.Equiv` `EquivLike.toFunLike` `instEquivLike`	—	—
`coe_toLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Representation.IntertwiningMap.toLinearMap` `toIntertwiningMap` `Representation.Equiv` `EquivLike.toFunLike` `instEquivLike`	—	—
`conj_apply_self` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.End` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.conj` `toLinearEquiv` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	`LinearMap.ext` `RingHomInvPair.ids` `smulCommClass_self` `RingHomCompTriple.ids` `Representation.IntertwiningMap.isIntertwining'` `apply_symm_apply`
`dualTensorHom_invFun` 📖	mathematical	—	`invFun` `TensorProduct` `Semifield.toCommSemiring` `Field.toSemifield` `Module.Dual` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Representation.tprod` `Representation.dual` `Representation.linHom` `dualTensorHom` `DFunLike.coe` `LinearEquiv` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `dualTensorHomEquivOfBasis` `Module.Free.ChooseBasisIndex` `Module.Free.instDecidableEqChooseBasisIndex` `Module.Free.ChooseBasisIndex.fintype` `Module.Free.chooseBasis`	—	`Algebra.to_smulCommClass` `smulCommClass_self`
`dualTensorHom_toFun` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `TensorProduct` `Semifield.toCommSemiring` `Field.toSemifield` `Module.Dual` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Representation.tprod` `Representation.dual` `Representation.linHom` `EquivLike.toFunLike` `instEquivLike` `dualTensorHom` `AddMonoidHom` `AddZeroClass.toAddZero` `instAddZeroClassTensorProduct` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `TensorProduct.liftAux` `LinearMap.smulRightₗ`	—	`Algebra.to_smulCommClass` `smulCommClass_self`
`ext` 📖	—	`DFunLike.coe` `Representation.Equiv` `EquivLike.toFunLike` `instEquivLike`	—	—	—
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `EquivLike.toFunLike` `instEquivLike`	—	`ext`
`instLinearEquivClass` 📖	mathematical	—	`LinearEquivClass` `Representation.Equiv` `instEquivLike`	—	`RingHomInvPair.ids` `LinearEquiv.map_add` `LinearEquiv.map_smul`
`left_inv` 📖	mathematical	—	`invFun` `AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap.toAddHom` `RingHom.id` `Semiring.toNonAssocSemiring` `Representation.IntertwiningMap.toLinearMap` `toIntertwiningMap`	—	—
`mk_apply` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `DFunLike.coe` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	`DFunLike.coe` `Representation.Equiv` `EquivLike.toFunLike` `instEquivLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DFinsupp.instEquivLikeLinearEquiv`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids`
`mk_symm` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `DFunLike.coe` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	`symm` `LinearEquiv.symm` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearEquiv.isIntertwining_symm_isIntertwining`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids`
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`right_inv` 📖	mathematical	—	`invFun` `AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap.toAddHom` `RingHom.id` `Semiring.toNonAssocSemiring` `Representation.IntertwiningMap.toLinearMap` `toIntertwiningMap`	—	—
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`left_inv`
`symm_trans` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `apply_symm_apply`
`toIntertwiningMap_mk'` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `DFunLike.coe` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	`toIntertwiningMap` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids`
`toIntertwiningMap_refl` 📖	mathematical	—	`toIntertwiningMap` `refl` `Representation.IntertwiningMap.id`	—	—
`toIntertwiningMap_trans` 📖	mathematical	—	`toIntertwiningMap` `trans` `Representation.IntertwiningMap.comp`	—	—
`toLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLinearEquiv` `Representation.IntertwiningMap` `Representation.IntertwiningMap.instFunLike` `toIntertwiningMap`	—	`RingHomInvPair.ids`
`toLinearEquiv_inj` 📖	mathematical	—	`toLinearEquiv`	—	`RingHomInvPair.ids` `toLinearEquiv_injective`
`toLinearEquiv_injective` 📖	mathematical	—	`Representation.Equiv` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `toLinearEquiv`	—	`RingHomInvPair.ids` `left_inv` `right_inv`
`toLinearEquiv_mk'` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `DFunLike.coe` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	`toLinearEquiv`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids`
`toLinearEquiv_toLinearMap` 📖	mathematical	—	`LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `toLinearEquiv` `Representation.IntertwiningMap.toLinearMap` `toIntertwiningMap`	—	`RingHomInvPair.ids`
`toLinearMap_mk'` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `DFunLike.coe` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	`Representation.IntertwiningMap.toLinearMap` `toIntertwiningMap` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids`
`toLinearMap_refl` 📖	mathematical	—	`Representation.IntertwiningMap.toLinearMap` `toIntertwiningMap` `refl` `LinearMap.id`	—	—
`toLinearMap_symm` 📖	mathematical	—	`Representation.IntertwiningMap.toLinearMap` `toIntertwiningMap` `symm` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearEquiv.symm` `toLinearEquiv`	—	—
`toLinearMap_trans` 📖	mathematical	—	`Representation.IntertwiningMap.toLinearMap` `toIntertwiningMap` `trans` `LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`trans_symm` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `symm_apply_apply`

Representation.IntertwiningMap

Definitions

Name	Category	Theorems
`centralMul` 📖	CompOp	—
`coeFnAddMonoidHom` 📖	CompOp	—
`comp` 📖	CompOp	28 math math: `comp_toLinearMap`, `comp_add`, `Representation.LinearizeMonoidal.ε_η`, `Representation.Equiv.toIntertwiningMap_trans`, `Rep.ofHom_comp`, `comp_apply`, `Representation.LinearizeMonoidal.μ_comp_assoc`, `Representation.LinearizeMonoidal.μ_comp_rTensor`, `Representation.LinearizeMonoidal.μ_δ`, `rTensor_comp_lTensor`, `Representation.LinearizeMonoidal.assoc_comp_δ`, `Representation.TensorProduct.comm_comp_rTensor`, `Representation.LinearizeMonoidal.rTensor_comp_δ`, `comp_def`, `Representation.LinearizeMonoidal.μ_comp_lTensor`, `Representation.LinearizeMonoidal.rightUnitor_δ`, `lTensor_comp_rTensor`, `add_comp`, `Representation.LinearizeMonoidal.leftUnitor_δ`, `Representation.TensorProduct.comm_comp_lTensor`, `Representation.LinearizeMonoidal.η_ε`, `Representation.LinearizeMonoidal.lTensor_comp_δ`, `Representation.LinearizeMonoidal.μ_leftUnitor`, `Representation.LinearizeMonoidal.μ_rightUnitor`, `Representation.LinearizeMonoidal.δ_μ`, `Rep.hom_comp`, `comp_smul`, `smul_comp`
`equivAlgEnd` 📖	CompOp	—
`equivLinearMapAsModule` 📖	CompOp	—
`id` 📖	CompOp	11 math math: `rTensor_id`, `toLinearMap_id`, `Representation.LinearizeMonoidal.ε_η`, `Rep.hom_id`, `Representation.LinearizeMonoidal.μ_δ`, `lTensor_id`, `Representation.Equiv.toIntertwiningMap_refl`, `id_apply`, `Representation.LinearizeMonoidal.η_ε`, `Representation.LinearizeMonoidal.δ_μ`, `Rep.ofHom_id`
`instAdd` 📖	CompOp	10 math math: `comp_add`, `Rep.add_hom`, `lTensor_add`, `tensor_add_left`, `Rep.ofHom_add`, `tensor_add_right`, `add_comp`, `coe_add`, `rTensor_add`, `add_toLinearMap`
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	14 math math: `Representation.card_inv_mul_sum_char_mul_char_eq_finrank`, `toLinearMap_sum`, `sum_apply`, `Representation.IsIrreducible.finrank_intertwiningMap_self`, `comp_def`, `Rep.sum_hom`, `Rep.ofHom_sum`, `instFiniteOfIsNoetherian`, `Representation.leftRegularMapEquiv_symm_single`, `Representation.freeLiftLEquiv_symm_apply`, `Representation.leftRegularMapEquiv_apply`, `Representation.freeLiftLEquiv_apply`, `toLinearMapl_apply`, `Representation.leftRegularMapEquiv_symm_apply_toFun`
`instAlgebra` 📖	CompOp	2 math math: `Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed`, `algebraMap_apply`
`instFunLike` 📖	CompOp	133 math math: `groupHomology.mapCycles₂_comp_assoc`, `mul_apply`, `groupHomology.coinvariantsMk_comp_H0Iso_inv_apply`, `groupHomology.chainsMap_f_3_comp_chainsIso₃_apply`, `Rep.resCoindToHom_hom_apply_coe`, `groupHomology.mapCycles₁_comp_apply`, `Representation.freeLift_single_single`, `instLinearMapClass`, `Representation.Equiv.coe_toIntertwiningMap`, `groupHomology.mapCycles₁_comp_assoc`, `Rep.preservesLimits_forget`, `groupHomology.π_comp_H0Iso_hom_assoc`, `Representation.LinearizeMonoidal.μ_apply_single_single`, `groupCohomology.mapShortComplexH2_comp_assoc`, `coe_toLinearMap`, `Rep.norm_comm_apply`, `comp_apply`, `coe_zero`, `coe_zsmul`, `FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ`, `Representation.equivOfIso_toFun`, `Rep.standardComplex.εToSingle₀_comp_eq`, `Rep.instEpiModuleCatAppCoinvariantsMk`, `Rep.forget_map`, `groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc`, `groupHomology.cyclesMap_comp_assoc`, `groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply`, `Rep.applyAsHom_comm_apply`, `groupHomology.chainsMap_f_single`, `Rep.coindFunctorIso_inv_app_hom_toFun_coe`, `Rep.instFaithfulModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier`, `groupHomology.coinvariantsMk_comp_H0Iso_inv`, `Rep.indToCoindAux_comm`, `groupHomology.map_comp_assoc`, `Representation.IsIrreducible.bijective_or_eq_zero`, `Rep.forget_obj`, `Representation.LinearizeMonoidal.ε_one`, `smul_apply`, `sum_apply`, `groupCohomology.cochainsMap_comp_assoc`, `groupHomology.pOpcycles_comp_opcyclesIso_hom_apply`, `groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply`, `Rep.subtype_hom_toFun`, `Rep.coinvariantsFunctor_hom_ext_iff`, `Representation.Equiv.toLinearEquiv_apply`, `Rep.mkIso_hom_hom_apply`, `groupCohomology.norm_ofAlgebraAutOnUnits_eq`, `groupHomology.d₁₀_comp_coinvariantsMk`, `groupHomology.mapCycles₂_comp_apply`, `Representation.IsIrreducible.injective_or_eq_zero`, `Rep.inv_hom_apply`, `Rep.mkIso_inv_hom_apply`, `groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply`, `Representation.coindMap_coe_apply_apply`, `Rep.preservesColimits_forget`, `Representation.LinearizeMonoidal.η_single`, `toLinearMap_apply`, `Representation.linHom.invariantsEquivRepHom_symm_apply_coe`, `coe_eq_toLinearMap`, `groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply`, `Representation.equivOfIso_invFun`, `id_apply`, `mem_ker`, `Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun`, `Rep.standardComplex.quasiIso_forget₂_εToSingle₀`, `Rep.leftRegularHom_hom_single`, `Rep.coinvariantsAdjunction_unit_app`, `Rep.coinvariantsMk_app_hom`, `Rep.forget₂_moduleCat_obj`, `groupCohomology.cocyclesMap_comp_assoc`, `groupHomology.pOpcycles_comp_opcyclesIso_hom`, `coe_add`, `groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv`, `Rep.instAdditiveModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier`, `coe_sub`, `FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ`, `lTensor_apply`, `Rep.leftRegularHomEquiv_symm_single`, `Rep.forget₂_moduleCat_map`, `Representation.LinearizeMonoidal.δ_apply_single`, `groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc`, `Rep.instLinearModuleCatForget₂IntertwiningMapVρLinearMapIdCarrier`, `Rep.norm_apply`, `Representation.linearizeMap_single`, `Rep.hom_comm_apply`, `Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply`, `Rep.standardComplex.d_apply`, `groupHomology.π_comp_H0Iso_hom`, `groupCohomology.mapShortComplexH1_comp_assoc`, `groupHomology.H0π_comp_H0Iso_hom`, `FDRep.forget₂_ρ`, `Rep.id_apply`, `Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq`, `mem_range`, `Rep.comp_apply`, `isIntertwining`, `coe_ofBijective`, `coe_neg`, `groupHomology.shortComplexH0_g`, `Rep.applyAsHom_apply`, `Rep.mkQ_hom_toFun`, `Representation.leftRegularMapEquiv_symm_single`, `Rep.epi_iff_surjective`, `groupHomology.d₁₀_comp_coinvariantsMk_assoc`, `groupHomology.chainsMap_f_0_comp_chainsIso₀_apply`, `groupHomology.H0π_comp_H0Iso_hom_assoc`, `Representation.coindMap_coe_apply`, `coe_mk`, `FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing`, `Rep.hom_inv_apply`, `Representation.LinearizeMonoidal.μ_apply_apply`, `Rep.coinvariantsAdjunction_homEquiv_apply_hom`, `Representation.leftRegularMapEquiv_apply`, `coe_nsmul`, `Representation.freeLiftLEquiv_apply`, `FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ`, `Rep.ofHom_apply`, `coe_smul`, `Rep.reflectsIsomorphisms_forget`, `groupHomology.H0π_comp_H0Iso_hom_apply`, `Rep.barComplex.d_single`, `Rep.mono_iff_injective`, `LinearMap.toIntertwiningMap`, `groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc`, `groupHomology.chainsMap_f_1_comp_chainsIso₁_apply`, `groupHomology.H0π_comp_map_apply`, `rTensor_apply`, `tensor_apply`, `Representation.leftRegularMapEquiv_symm_apply_toFun`, `groupHomology.chainsMap_f_2_comp_chainsIso₂_apply`, `coe_one`, `groupCohomology.map_comp_assoc`, `Rep.coindFunctorIso_hom_app_hom_toFun_hom_toFun`
`instModule` 📖	CompOp	10 math math: `Representation.card_inv_mul_sum_char_mul_char_eq_finrank`, `Representation.IsIrreducible.finrank_intertwiningMap_self`, `comp_def`, `instFiniteOfIsNoetherian`, `Representation.leftRegularMapEquiv_symm_single`, `Representation.freeLiftLEquiv_symm_apply`, `Representation.leftRegularMapEquiv_apply`, `Representation.freeLiftLEquiv_apply`, `toLinearMapl_apply`, `Representation.leftRegularMapEquiv_symm_apply_toFun`
`instMonoid` 📖	CompOp	—
`instMul` 📖	CompOp	2 math math: `mul_apply`, `coe_mul`
`instNatCast` 📖	CompOp	—
`instNeg` 📖	CompOp	3 math math: `coe_neg`, `Rep.ofHom_neg`, `Rep.neg_hom`
`instOne` 📖	CompOp	2 math math: `algebraMap_apply`, `coe_one`
`instPowNat` 📖	CompOp	—
`instSMul` 📖	CompOp	12 math math: `tensor_smul_right`, `smul_apply`, `algebraMap_apply`, `Rep.smul_hom`, `toLinearMap_smul`, `rTensor_smul`, `tensor_smul_left`, `lTensor_smul`, `comp_smul`, `coe_smul`, `smul_comp`, `Rep.ofHom_smul`
`instSMulInt` 📖	CompOp	3 math math: `coe_zsmul`, `Rep.zsmul_hom`, `Rep.ofHom_zsmul`
`instSMulNat` 📖	CompOp	3 math math: `Rep.nsmul_hom`, `Rep.ofHom_nsmul`, `coe_nsmul`
`instSemigroup` 📖	CompOp	—
`instSemiring` 📖	CompOp	2 math math: `Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed`, `algebraMap_apply`
`instSub` 📖	CompOp	4 math math: `Rep.ofHom_sub`, `sub_toLinearMap`, `Rep.sub_hom`, `coe_sub`
`instZero` 📖	CompOp	8 math math: `rTensor_zero`, `coe_zero`, `Representation.IsIrreducible.bijective_or_eq_zero`, `lTensor_zero`, `Representation.IsIrreducible.injective_or_eq_zero`, `Rep.zero_hom`, `zero_toLinearMap`, `Rep.ofHom_zero`
`ker` 📖	CompOp	2 math math: `mem_ker`, `ker_toSubmodule`
`lTensor` 📖	CompOp	17 math math: `lTensor_add`, `Representation.LinearizeMonoidal.μ_comp_assoc`, `lTensor_id`, `rTensor_comp_lTensor`, `lTensor_zero`, `Representation.LinearizeMonoidal.assoc_comp_δ`, `Representation.TensorProduct.comm_comp_rTensor`, `Representation.LinearizeMonoidal.μ_comp_lTensor`, `Representation.LinearizeMonoidal.rightUnitor_δ`, `lTensor_comp_rTensor`, `toLinearMap_lTensor`, `Representation.TensorProduct.comm_comp_lTensor`, `lTensor_apply`, `Representation.LinearizeMonoidal.lTensor_comp_δ`, `Representation.LinearizeMonoidal.μ_rightUnitor`, `lTensor_smul`, `Rep.hom_whiskerLeft`
`llcomp` 📖	CompOp	1 math math: `comp_def`
`ofBijective` 📖	CompOp	1 math math: `coe_ofBijective`
`rTensor` 📖	CompOp	17 math math: `rTensor_zero`, `rTensor_id`, `Rep.hom_whiskerRight`, `Representation.LinearizeMonoidal.μ_comp_assoc`, `Representation.LinearizeMonoidal.μ_comp_rTensor`, `toLinearMap_rTensor`, `rTensor_comp_lTensor`, `Representation.LinearizeMonoidal.assoc_comp_δ`, `Representation.TensorProduct.comm_comp_rTensor`, `Representation.LinearizeMonoidal.rTensor_comp_δ`, `rTensor_smul`, `lTensor_comp_rTensor`, `Representation.LinearizeMonoidal.leftUnitor_δ`, `Representation.TensorProduct.comm_comp_lTensor`, `Representation.LinearizeMonoidal.μ_leftUnitor`, `rTensor_add`, `rTensor_apply`
`range` 📖	CompOp	2 math math: `range_toSubmodule`, `mem_range`
`tensor` 📖	CompOp	9 math math: `tensor_add_left`, `tensor_smul_right`, `rTensor_comp_lTensor`, `tensor_add_right`, `lTensor_comp_rTensor`, `tensor_smul_left`, `toLinearMap_tensor`, `Rep.hom_tensorHom`, `tensor_apply`
`toLinearMap` 📖	CompOp	109 math math: `comp_toLinearMap`, `Rep.invariantsAdjunction_homEquiv_symm_apply_hom`, `Rep.MonoidalClosed.linearHomEquiv_symm_hom`, `Representation.Equiv.toLinearMap_refl`, `groupHomology.chainsMap_f_3_comp_chainsIso₃_apply`, `groupHomology.mapCycles₁_comp_apply`, `toLinearMap_id`, `Representation.Equiv.toLinearEquiv_toLinearMap`, `toLinearMap_injective`, `toLinearMap_mk`, `coe_mul`, `groupCohomology.map_H0Iso_hom_f_apply`, `Representation.ofMulActionSubsingletonEquivTrivial_symm_apply`, `Rep.standardComplex.d_eq`, `Representation.TensorProduct.assoc_symm_toLinearMap`, `Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff`, `coe_toLinearMap`, `groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply`, `groupCohomology.mapCocycles₂_comp_i_apply`, `groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply`, `groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply`, `Rep.ihom_ev_app_hom`, `Rep.MonoidalClosed.linearHomEquivComm_hom`, `Rep.coindVEquiv_symm_apply_coe`, `Rep.liftHomOfSurj_toLinearMap`, `sub_toLinearMap`, `Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff`, `Rep.tensorHomEquiv_apply`, `toLinearMap_sum`, `Representation.ofMulActionSubsingletonEquivTrivial_apply`, `Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff`, `Rep.res_map_hom_toLinearMap`, `range_toSubmodule`, `toLinearMap_rTensor`, `groupHomology.mapCycles₁_comp_i_apply`, `Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff`, `ext_iff`, `Representation.LinearizeMonoidal.η_toLinearMap`, `Rep.mkIso_hom_hom_apply`, `Rep.hom_comp_toLinearMap`, `groupHomology.mapCycles₂_comp_apply`, `Rep.resCoindHomEquiv_symm_apply`, `Representation.Equiv.right_inv`, `toLinearMap_smul`, `groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply`, `Representation.freeLift_toLinearMap`, `groupCohomology.map_id_comp_H0Iso_hom_apply`, `groupHomology.chainsMap_id_f_hom_eq_mapRange`, `Representation.Equiv.toLinearMap_mk'`, `toLinearMap_apply`, `coe_eq_toLinearMap`, `groupHomology.lsingle_comp_chainsMap_f`, `groupCohomology.cochainsMap_f`, `Rep.coind'_ext_iff`, `toFun_injective`, `Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff`, `Rep.mkIso_inv_hom_toLinearMap`, `isIntertwining'`, `toLinearMap_lTensor`, `Rep.indCoindIso_hom_hom_toLinearMap`, `Representation.Equiv.left_inv`, `Representation.TensorProduct.toLinearMap_assoc`, `Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff`, `Rep.indResHomEquiv_apply`, `Rep.indCoindIso_inv_hom_toLinearMap`, `Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm`, `groupHomology.chainsMap_f_hom`, `Rep.forget₂_moduleCat_map`, `groupHomology.map_id_comp_H0Iso_hom_apply`, `isIntertwining_assoc`, `groupCohomology.mapCocycles₁_comp_i_apply`, `Rep.MonoidalClosed.linearHomEquiv_hom`, `Rep.invariantsAdjunction_homEquiv_apply_hom`, `Representation.LinearizeMonoidal.μ_toLinearMap`, `groupCohomology.cochainsMap_f_hom`, `Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff`, `Rep.quotientToCoinvariantsFunctor_map_hom_toLinearMap`, `Rep.ihom_map`, `Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub`, `Rep.invariantsFunctor_map_hom`, `toLinearMap_tensor`, `Rep.ihom_coev_app_hom`, `Rep.indResHomEquiv_symm_apply`, `groupHomology.mapCycles₂_comp_i_apply`, `Representation.linearizeMap_toLinearMap`, `zero_toLinearMap`, `Rep.MonoidalClosed.linearHomEquivComm_symm_hom`, `Representation.coindMap_coe_apply`, `groupHomology.lsingle_comp_chainsMap_f_assoc`, `Representation.Equiv.toLinearMap_symm`, `Rep.tensorHomEquiv_symm_apply`, `groupCohomology.cochainsMap_id_f_hom_eq_compLeft`, `Rep.coinvariantsAdjunction_homEquiv_apply_hom`, `Representation.TensorProduct.toLinearMap_rid`, `add_toLinearMap`, `Rep.coinvariantsFunctor_map_hom`, `Representation.Equiv.toLinearMap_trans`, `groupHomology.chainsMap_f_1_comp_chainsIso₁_apply`, `Rep.mkIso_hom_hom_toLinearMap`, `Representation.TensorProduct.toLinearMap_comm`, `toLinearMapl_apply`, `Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination`, `Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff`, `Representation.Equiv.coe_toLinearMap`, `Representation.TensorProduct.toLinearMap_lid`, `Representation.LinearizeMonoidal.ε_toLinearMap`, `groupHomology.chainsMap_f`, `groupHomology.chainsMap_f_2_comp_chainsIso₂_apply`, `ker_toSubmodule`
`toLinearMapl` 📖	CompOp	1 math math: `toLinearMapl_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_comp` 📖	mathematical	—	`comp` `Representation.IntertwiningMap` `instAdd`	—	`ext` `RingHomCompTriple.ids` `LinearMap.comp_add`
`add_toLinearMap` 📖	mathematical	—	`toLinearMap` `Representation.IntertwiningMap` `instAdd` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instAdd`	—	—
`algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `instSMul` `instOne`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `instFunLike` `instAdd` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`coe_eq_toLinearMap` 📖	mathematical	—	`SemilinearMapClass.semilinearMap` `Representation.IntertwiningMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `instLinearMapClass` `toLinearMap`	—	`instLinearMapClass`
`coe_mk` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	`DFunLike.coe` `Representation.IntertwiningMap` `instFunLike` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`RingHomCompTriple.ids`
`coe_mul` 📖	mathematical	—	`toLinearMap` `CommSemiring.toSemiring` `Representation.IntertwiningMap` `instMul` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End.instMul`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `AddCommGroup.toAddCommMonoid` `instFunLike` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`coe_nsmul` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `instFunLike` `instSMulNat` `AddMonoid.toNSMul` `Pi.addMonoid` `AddCommMonoid.toAddMonoid`	—	—
`coe_ofBijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instFunLike`	`DFunLike.coe` `Representation.Equiv` `CommSemiring.toSemiring` `EquivLike.toFunLike` `Representation.Equiv.instEquivLike` `ofBijective` `Representation.IntertwiningMap` `instFunLike`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instFunLike` `instOne`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instFunLike` `instSMul` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `AddCommGroup.toAddCommMonoid` `instFunLike` `instSub` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`coe_toLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `toLinearMap` `Representation.IntertwiningMap` `instFunLike`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `instFunLike` `instZero` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`coe_zsmul` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `AddCommGroup.toAddCommMonoid` `instFunLike` `instSMulInt` `SubNegMonoid.toZSMul` `Pi.subNegMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`comp_add` 📖	mathematical	—	`comp` `Representation.IntertwiningMap` `instAdd`	—	`ext` `RingHomCompTriple.ids`
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `instFunLike` `comp`	—	—
`comp_def` 📖	mathematical	—	`comp` `CommSemiring.toSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Representation.IntertwiningMap` `instAddCommMonoid` `instModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `llcomp`	—	—
`comp_smul` 📖	mathematical	—	`comp` `CommSemiring.toSemiring` `Representation.IntertwiningMap` `instSMul`	—	`smulCommClass_self` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`comp_toLinearMap` 📖	mathematical	—	`toLinearMap` `comp` `LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	—
`ext` 📖	—	`toLinearMap`	—	—	`RingHomCompTriple.ids`
`ext_iff` 📖	mathematical	—	`toLinearMap`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `instFunLike` `id`	—	—
`instFiniteOfIsNoetherian` 📖	mathematical	—	`Module.Finite` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommMonoid` `instModule`	—	`Module.Finite.of_injective` `smulCommClass_self` `isNoetherian_linearMap` `RingHomInvPair.ids` `toLinearMap_injective`
`instLinearMapClass` 📖	mathematical	—	`LinearMapClass` `Representation.IntertwiningMap` `instFunLike`	—	`LinearMap.map_add` `LinearMap.map_smul`
`isIntertwining` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `instFunLike` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Representation` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	`RingHomCompTriple.ids` `isIntertwining'`
`isIntertwining'` 📖	mathematical	—	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `toLinearMap` `DFunLike.coe` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	—
`isIntertwiningMap_of_mem_center` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.center`	`Representation.IsIntertwiningMap` `CommSemiring.toSemiring` `DFunLike.coe` `Representation` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	`Representation.isIntertwiningMap_iff` `Module.End.mul_apply` `MonoidHom.map_mul` `Submonoid.mem_center_iff`
`isIntertwining_assoc` 📖	mathematical	—	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `toLinearMap` `DFunLike.coe` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	`RingHomCompTriple.ids` `LinearMap.comp_assoc` `isIntertwining'`
`ker_toSubmodule` 📖	mathematical	—	`Subrepresentation.toSubmodule` `ker` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `toLinearMap`	—	—
`lTensor_add` 📖	mathematical	—	`lTensor` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instAdd` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`tensor_add_right`
`lTensor_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `instFunLike` `lTensor` `TensorProduct.tmul`	—	—
`lTensor_comp_rTensor` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `lTensor` `rTensor` `tensor`	—	`ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `LinearMap.lTensor_comp_rTensor`
`lTensor_id` 📖	mathematical	—	`lTensor` `id` `CommSemiring.toSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `LinearMap.lTensor_id`
`lTensor_smul` 📖	mathematical	—	`lTensor` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instSMul` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`tensor_smul_right`
`lTensor_zero` 📖	mathematical	—	`lTensor` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instZero` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `LinearMap.lTensor_zero`
`mem_ker` 📖	mathematical	—	`Subrepresentation` `SetLike.instMembership` `Subrepresentation.instSetLike` `ker` `DFunLike.coe` `Representation.IntertwiningMap` `instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`mem_range` 📖	mathematical	—	`Subrepresentation` `SetLike.instMembership` `Subrepresentation.instSetLike` `range` `DFunLike.coe` `Representation.IntertwiningMap` `instFunLike`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instFunLike` `instMul`	—	—
`rTensor_add` 📖	mathematical	—	`rTensor` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instAdd` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`tensor_add_left`
`rTensor_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `instFunLike` `rTensor` `TensorProduct.tmul`	—	—
`rTensor_comp_lTensor` 📖	mathematical	—	`comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `rTensor` `lTensor` `tensor`	—	`ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `LinearMap.rTensor_comp_lTensor`
`rTensor_id` 📖	mathematical	—	`rTensor` `id` `CommSemiring.toSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `LinearMap.rTensor_id`
`rTensor_smul` 📖	mathematical	—	`rTensor` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instSMul` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`tensor_smul_left`
`rTensor_zero` 📖	mathematical	—	`rTensor` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instZero` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `LinearMap.rTensor_zero`
`range_toSubmodule` 📖	mathematical	—	`Subrepresentation.toSubmodule` `range` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `toLinearMap`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instFunLike` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`smul_comp` 📖	mathematical	—	`comp` `CommSemiring.toSemiring` `Representation.IntertwiningMap` `instSMul`	—	`smulCommClass_self` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`sub_toLinearMap` 📖	mathematical	—	`toLinearMap` `AddCommGroup.toAddCommMonoid` `Representation.IntertwiningMap` `instSub` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instSub`	—	—
`sum_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `instFunLike` `Finset.sum` `instAddCommMonoid`	—	`toLinearMap_apply` `toLinearMap_sum` `LinearMap.sum_apply` `Finset.sum_congr`
`tensor_add_left` 📖	mathematical	—	`tensor` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instAdd` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `TensorProduct.add_tmul`
`tensor_add_right` 📖	mathematical	—	`tensor` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instAdd` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `TensorProduct.tmul_add`
`tensor_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `instFunLike` `tensor` `TensorProduct.tmul`	—	—
`tensor_smul_left` 📖	mathematical	—	`tensor` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instSMul` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `smulCommClass_self` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `TensorProduct.tmul_smul`
`tensor_smul_right` 📖	mathematical	—	`tensor` `Representation.IntertwiningMap` `CommSemiring.toSemiring` `instSMul` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod`	—	`ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `smulCommClass_self` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower`
`toFun_injective` 📖	mathematical	—	`Representation.IntertwiningMap` `AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap.toAddHom` `RingHom.id` `Semiring.toNonAssocSemiring` `toLinearMap`	—	`ext` `LinearMap.ext`
`toLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `toLinearMap` `Representation.IntertwiningMap` `instFunLike`	—	—
`toLinearMap_id` 📖	mathematical	—	`toLinearMap` `id` `LinearMap.id`	—	—
`toLinearMap_injective` 📖	mathematical	—	`Representation.IntertwiningMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `toLinearMap`	—	`ext`
`toLinearMap_lTensor` 📖	mathematical	—	`toLinearMap` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `lTensor` `LinearMap.lTensor`	—	—
`toLinearMap_mk` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `Representation` `LinearMap` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	`toLinearMap`	—	`RingHomCompTriple.ids`
`toLinearMap_rTensor` 📖	mathematical	—	`toLinearMap` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `rTensor` `LinearMap.rTensor`	—	—
`toLinearMap_smul` 📖	mathematical	—	`toLinearMap` `CommSemiring.toSemiring` `Representation.IntertwiningMap` `instSMul` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid`	—	—
`toLinearMap_sum` 📖	mathematical	—	`toLinearMap` `Finset.sum` `Representation.IntertwiningMap` `instAddCommMonoid` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid`	—	`Finset.induction` `Finset.sum_insert`
`toLinearMap_tensor` 📖	mathematical	—	`toLinearMap` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `tensor` `TensorProduct.map` `RingHom.id` `Semiring.toNonAssocSemiring`	—	—
`toLinearMapl_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Representation.IntertwiningMap` `instAddCommMonoid` `LinearMap.addCommMonoid` `instModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `toLinearMapl` `toLinearMap`	—	`smulCommClass_self`
`zero_toLinearMap` 📖	mathematical	—	`toLinearMap` `Representation.IntertwiningMap` `instZero` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instZero`	—	—

Representation.IsIntertwiningMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntertwining` 📖	mathematical	`Representation.IsIntertwiningMap`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Representation` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	—

Representation.TensorProduct

Definitions

Name	Category	Theorems
`assoc` 📖	CompOp	7 math math: `Rep.hom_hom_associator`, `assoc_symm_toLinearMap`, `Representation.LinearizeMonoidal.μ_comp_assoc`, `Representation.LinearizeMonoidal.assoc_comp_δ`, `toLinearMap_assoc`, `Rep.hom_inv_associator`, `assoc_apply`
`comm` 📖	CompOp	6 math math: `Rep.hom_braiding`, `comm_comp_rTensor`, `comm_apply`, `comm_comp_lTensor`, `comm_symm`, `toLinearMap_comm`
`lid` 📖	CompOp	7 math math: `Rep.hom_hom_leftUnitor`, `Representation.LinearizeMonoidal.leftUnitor_δ`, `Representation.LinearizeMonoidal.μ_leftUnitor`, `Rep.hom_inv_leftUnitor`, `lid_symm_apply`, `lid_apply`, `toLinearMap_lid`
`rid` 📖	CompOp	7 math math: `rid_symm_apply`, `rid_apply`, `Representation.LinearizeMonoidal.rightUnitor_δ`, `Rep.hom_inv_rightUnitor`, `Rep.hom_hom_rightUnitor`, `Representation.LinearizeMonoidal.μ_rightUnitor`, `toLinearMap_rid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `CommSemiring.toSemiring` `Representation.tprod` `EquivLike.toFunLike` `Representation.Equiv.instEquivLike` `assoc` `TensorProduct.tmul`	—	—
`assoc_symm_toLinearMap` 📖	mathematical	—	`Representation.IntertwiningMap.toLinearMap` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `CommSemiring.toSemiring` `Representation.tprod` `Representation.Equiv.toIntertwiningMap` `Representation.Equiv.symm` `assoc` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearEquiv.symm` `TensorProduct.assoc`	—	—
`comm_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `EquivLike.toFunLike` `Representation.Equiv.instEquivLike` `comm` `TensorProduct.tmul`	—	—
`comm_comp_lTensor` 📖	mathematical	—	`Representation.IntertwiningMap.comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `Representation.Equiv.toIntertwiningMap` `comm` `Representation.IntertwiningMap.lTensor` `Representation.IntertwiningMap.rTensor`	—	`Representation.IntertwiningMap.ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass`
`comm_comp_rTensor` 📖	mathematical	—	`Representation.IntertwiningMap.comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `Representation.Equiv.toIntertwiningMap` `comm` `Representation.IntertwiningMap.rTensor` `Representation.IntertwiningMap.lTensor`	—	`Representation.IntertwiningMap.ext` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass`
`comm_symm` 📖	mathematical	—	`Representation.Equiv.symm` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `comm`	—	—
`lid_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `Representation.trivial` `EquivLike.toFunLike` `Representation.Equiv.instEquivLike` `lid` `TensorProduct.tmul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`lid_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `Representation.trivial` `EquivLike.toFunLike` `Representation.Equiv.instEquivLike` `Representation.Equiv.symm` `lid` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`rid_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `Representation.trivial` `EquivLike.toFunLike` `Representation.Equiv.instEquivLike` `rid` `TensorProduct.tmul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`rid_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Representation.Equiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `Representation.trivial` `EquivLike.toFunLike` `Representation.Equiv.instEquivLike` `Representation.Equiv.symm` `rid` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`toLinearMap_assoc` 📖	mathematical	—	`Representation.IntertwiningMap.toLinearMap` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `CommSemiring.toSemiring` `Representation.tprod` `Representation.Equiv.toIntertwiningMap` `assoc` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct.assoc`	—	—
`toLinearMap_comm` 📖	mathematical	—	`Representation.IntertwiningMap.toLinearMap` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `Representation.Equiv.toIntertwiningMap` `comm` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct.comm`	—	—
`toLinearMap_lid` 📖	mathematical	—	`Representation.IntertwiningMap.toLinearMap` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `Representation.trivial` `Representation.Equiv.toIntertwiningMap` `lid` `LinearEquiv.toLinearMap` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.lid`	—	—
`toLinearMap_rid` 📖	mathematical	—	`Representation.IntertwiningMap.toLinearMap` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Representation.tprod` `Representation.trivial` `Representation.Equiv.toIntertwiningMap` `rid` `LinearEquiv.toLinearMap` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.rid`	—	—

---

← Back to Index