Associator

📁 Source: Mathlib/LinearAlgebra/TensorProduct/Associator.lean

Statistics

Metric	Count
Definitions assoc, leftComm, lid, lidOfCompatibleSMul, rid, rightComm, tensorTensorTensorAssoc, tensorTensorTensorComm	8
Theorems tensorProductAssoc_def, lTensor_rTensor_comp_assoc, lTensor_tensor, lid_comp_rTensor, rTensor_lTensor_comp_assoc_symm, rTensor_tensor, rid_comp_lTensor, assoc_symm_tmul, assoc_tensor, assoc_tensor', assoc_tensor'', assoc_tmul, comm_trans_lid, comm_trans_rid, includeRight_lid, leftComm_def, leftComm_symm_tmul, leftComm_tmul, lidOfCompatibleSMul_tmul, lid_eq_rid, lid_symm_apply, lid_tensor, lid_tmul, map_map_assoc, map_map_assoc_symm, map_map_comp_assoc_eq, map_map_comp_assoc_symm_eq, rid_symm_apply, rid_tmul, rightComm_def, rightComm_symm, rightComm_tmul, tensorTensorTensorAssoc_symm_tmul, tensorTensorTensorAssoc_tmul, tensorTensorTensorComm_comp_map, tensorTensorTensorComm_symm, tensorTensorTensorComm_tmul, tensorTensorTensorComm_trans_tensorTensorTensorComm, toLinearMap_symm_lid, toLinearMap_symm_rid	40
Total	48

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensorProductAssoc_def 📖	mathematical	—	TensorProduct.assoc addCommMonoid module CommSemiring.toSemiring LinearEquiv.trans TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids TensorProduct.congr linearEquiv LinearEquiv.symm	—	LinearEquiv.ext RingHomInvPair.ids RingHomCompTriple.ids TensorProduct.induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass TensorProduct.zero_tmul LinearEquiv.symm_apply_apply TensorProduct.add_tmul map_add SemilinearMapClass.toAddHomClass

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lTensor_rTensor_comp_assoc 📖	mathematical	—	comp TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lTensor rTensor LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.assoc	—	RingHomCompTriple.ids RingHomInvPair.ids TensorProduct.map_map_comp_assoc_eq
lTensor_tensor 📖	mathematical	—	lTensor TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm TensorProduct.assoc	—	TensorProduct.ext RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self
lid_comp_rTensor 📖	mathematical	—	comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.lid rTensor TensorProduct.lift LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction lsmul	—	TensorProduct.ext' RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self
rTensor_lTensor_comp_assoc_symm 📖	mathematical	—	comp TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids rTensor lTensor LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm TensorProduct.assoc	—	RingHomCompTriple.ids RingHomInvPair.ids TensorProduct.map_map_comp_assoc_symm_eq
rTensor_tensor 📖	mathematical	—	rTensor TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.assoc LinearEquiv.symm	—	TensorProduct.ext RingHomCompTriple.ids RingHomInvPair.ids ext smulCommClass_self
rid_comp_lTensor 📖	mathematical	—	comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.rid lTensor TensorProduct.lift compl₂ SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid flip lsmul	—	TensorProduct.ext' RingHomCompTriple.ids RingHomInvPair.ids SMulCommClass.symm smulCommClass_self

TensorProduct

Definitions

Name	Category	Theorems
assoc 📖	CompOp	47 math math: LinearMap.lTensor_rTensor_comp_assoc, CoalgCat.MonoidalCategoryAux.associator_hom_toLinearMap, Coalgebra.coassoc_symm_apply, contractLeft_assoc_coevaluation, Matrix.kroneckerTMul_assoc', gradedMul_def, toMatrix_assoc, QuadraticForm.tensorAssoc_toLinearEquiv, map_map_assoc_symm, leftComm_def, LinearMap.rTensor_lTensor_comp_assoc_symm, map_map_comp_assoc_eq, norm_assoc, assoc_tmul, ModuleCat.hom_inv_associator, ModuleCat.MonoidalCategory.associator_def, QuadraticForm.tmul_tensorAssoc_apply, SemimoduleCat.hom_inv_associator, inner_assoc_assoc, Equiv.tensorProductAssoc_def, QuadraticForm.tensorAssoc_symm_apply, Coalgebra.coassoc, assocIsometry_apply, ModuleCat.hom_hom_associator, assoc_tensor'', enorm_assoc, SemimoduleCat.hom_hom_associator, toLinearEquiv_assocIsometry, nnnorm_assoc, Module.Invertible.rTensorEquiv_symm_apply_apply, map_map_assoc, QuadraticForm.tensorAssoc_apply, Coalgebra.coassoc_apply, Coalgebra.coassoc_symm, map_map_comp_assoc_symm_eq, Matrix.kroneckerTMul_assoc, assoc_tensor, QuadraticForm.tmul_comp_tensorAssoc, assoc_tensor', assoc_symm_tmul, LinearMap.lTensor_tensor, rightComm_def, contractLeft_assoc_coevaluation', assocIsometry_symm_apply, AlgebraTensorModule.assoc_eq, lid_tensor, LinearMap.rTensor_tensor
leftComm 📖	CompOp	5 math math: AlgebraTensorModule.leftComm_eq, leftComm_tmul, leftComm_def, Algebra.TensorProduct.leftComm_toLinearEquiv, leftComm_symm_tmul
lid 📖	CompOp	37 math math: enorm_lid, toLinearEquiv_lidIsometry, contractLeft_assoc_coevaluation, quotTensorEquivQuotSMul_comp_mkQ_rTensor, lidIsometry_apply, comm_trans_lid, inner_lid_lid, QuadraticForm.comp_tensorLId_eq, lid_symm_apply, lid_tmul, SemimoduleCat.hom_inv_leftUnitor, ModuleCat.hom_hom_leftUnitor, QuadraticForm.tensorLId_toLinearEquiv, CoalgCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMap, QuadraticForm.tensorLId_symm_apply, QuadraticForm.tmul_tensorLId_apply, QuadraticForm.tensorLId_apply, norm_lid, lid_eq_rid, Ideal.pi_mkQ_rTensor, Coalgebra.TensorProduct.lid_toLinearEquiv, toLinearMap_symm_lid, ModuleCat.MonoidalCategory.leftUnitor_def, ModuleCat.hom_inv_leftUnitor, Submodule.map_range_rTensor_subtype_lid, equivFinsuppOfBasisLeft_apply, SemimoduleCat.hom_hom_leftUnitor, LinearMap.lid_comp_rTensor, finsuppScalarLeft_apply, PolynomialLaw.ground_apply, nnnorm_lid, Algebra.TensorProduct.lid_toLinearEquiv, comm_trans_rid, contractLeft_assoc_coevaluation', dualDistribEquivOfBasis_apply_apply, lid_tensor, includeRight_lid
lidOfCompatibleSMul 📖	CompOp	1 math math: lidOfCompatibleSMul_tmul
rid 📖	CompOp	23 math math: contractLeft_assoc_coevaluation, SemimoduleCat.hom_inv_rightUnitor, tensorQuotEquivQuotSMul_comp_mkQ_lTensor, comm_trans_lid, QuadraticForm.tensorRId_symm_apply, SemimoduleCat.hom_hom_rightUnitor, QuadraticForm.tensorRId_apply, ModuleCat.MonoidalCategory.rightUnitor_def, ModuleCat.hom_hom_rightUnitor, QuadraticForm.tmul_tensorRId_apply, AlgebraTensorModule.rid_eq_rid, ModuleCat.hom_inv_rightUnitor, rid_tmul, QuadraticForm.tensorRId_toLinearEquiv, QuadraticForm.comp_tensorRId_eq, equivFinsuppOfBasisRight_apply, rid_symm_apply, lid_eq_rid, LinearMap.rid_comp_lTensor, toLinearMap_symm_rid, CoalgCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap, comm_trans_rid, contractLeft_assoc_coevaluation'
rightComm 📖	CompOp	4 math math: AlgebraTensorModule.rightComm_eq, rightComm_symm, rightComm_tmul, rightComm_def
tensorTensorTensorAssoc 📖	CompOp	2 math math: tensorTensorTensorAssoc_symm_tmul, tensorTensorTensorAssoc_tmul
tensorTensorTensorComm 📖	CompOp	11 math math: tensorTensorTensorComm_tmul, tensorTensorTensorComm_comp_map, tensorTensorTensorComm_symm, CoalgCat.MonoidalCategoryAux.tensorObj_comul, Algebra.TensorProduct.toLinearEquiv_tensorTensorTensorComm, AlgebraTensorModule.tensorTensorTensorComm_eq, ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, SemimoduleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, tensorTensorTensorComm_trans_tensorTensorTensorComm, LinearMap.mul'_tensor, Algebra.mul'_comp_tensorTensorTensorComm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc_symm_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm assoc tmul	—	RingHomInvPair.ids
assoc_tensor 📖	mathematical	—	assoc TensorProduct addCommMonoid instModule LinearEquiv.trans CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids LinearEquiv.rTensor LinearEquiv.lTensor LinearEquiv.symm	—	RingHomInvPair.ids RingHomCompTriple.ids ext_fourfold
assoc_tensor' 📖	mathematical	—	assoc TensorProduct addCommMonoid instModule LinearEquiv.trans CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids LinearEquiv.rTensor LinearEquiv.symm LinearEquiv.lTensor	—	RingHomInvPair.ids RingHomCompTriple.ids ext_fourfold''
assoc_tensor'' 📖	mathematical	—	assoc TensorProduct addCommMonoid instModule LinearEquiv.trans CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids LinearEquiv.symm LinearEquiv.rTensor LinearEquiv.lTensor	—	RingHomInvPair.ids RingHomCompTriple.ids ext_fourfold'
assoc_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike assoc tmul	—	RingHomInvPair.ids
comm_trans_lid 📖	mathematical	—	LinearEquiv.trans TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule addCommMonoid instModule RingHom.id RingHomCompTriple.ids RingHomInvPair.ids comm lid rid	—	LinearEquiv.toLinearMap_injective RingHomInvPair.ids RingHomCompTriple.ids ext LinearMap.ext smulCommClass_self LinearMap.ext_ring
comm_trans_rid 📖	mathematical	—	LinearEquiv.trans TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule addCommMonoid instModule RingHom.id RingHomCompTriple.ids RingHomInvPair.ids comm rid lid	—	LinearEquiv.toLinearMap_injective RingHomInvPair.ids RingHomCompTriple.ids ext LinearMap.ext_ring smulCommClass_self LinearMap.ext
includeRight_lid 📖	mathematical	—	tmul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id RingHomInvPair.ids TensorProduct Semiring.toModule addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike lid LinearMap Algebra.id LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap Algebra.algHom IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	RingHomCompTriple.ids IsScalarTower.left RingHomInvPair.ids map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass LinearEquiv.symm_apply_apply
leftComm_def 📖	mathematical	—	leftComm LinearEquiv.trans TensorProduct addCommMonoid instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids LinearEquiv.symm assoc congr comm LinearEquiv.refl	—	LinearEquiv.toLinearMap_injective RingHomInvPair.ids RingHomCompTriple.ids ext LinearMap.ext smulCommClass_self
leftComm_symm_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm leftComm tmul	—	RingHomInvPair.ids
leftComm_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike leftComm tmul	—	RingHomInvPair.ids
lidOfCompatibleSMul_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring addCommMonoid leftModule Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike lidOfCompatibleSMul tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids
lid_eq_rid 📖	mathematical	—	lid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule rid	—	LinearEquiv.toLinearMap_injective RingHomInvPair.ids ext' mul_comm
lid_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm lid tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids
lid_tensor 📖	mathematical	—	lid TensorProduct addCommMonoid instModule LinearEquiv.trans NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule RingHom.id RingHomCompTriple.ids RingHomInvPair.ids LinearEquiv.symm assoc LinearEquiv.rTensor	—	RingHomInvPair.ids RingHomCompTriple.ids ext_threefold'
lid_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike lid tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids
map_map_assoc 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct addCommMonoid instModule LinearMap.instFunLike map LinearEquiv RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike assoc	—	DFunLike.congr_fun RingHomCompTriple.ids RingHomInvPair.ids map_map_comp_assoc_eq
map_map_assoc_symm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct addCommMonoid instModule LinearMap.instFunLike map LinearEquiv RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm assoc	—	DFunLike.congr_fun RingHomCompTriple.ids RingHomInvPair.ids map_map_comp_assoc_symm_eq
map_map_comp_assoc_eq 📖	mathematical	—	LinearMap.comp TensorProduct addCommMonoid instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids map LinearEquiv.toLinearMap RingHomInvPair.ids assoc	—	ext RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_self LinearMap.ext
map_map_comp_assoc_symm_eq 📖	mathematical	—	LinearMap.comp TensorProduct addCommMonoid instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids map LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm assoc	—	ext RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext smulCommClass_self
rid_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm rid tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids
rid_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike rid tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids
rightComm_def 📖	mathematical	—	rightComm LinearEquiv.trans TensorProduct addCommMonoid instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids assoc congr LinearEquiv.refl comm LinearEquiv.symm	—	LinearEquiv.toLinearMap_injective RingHomInvPair.ids RingHomCompTriple.ids ext smulCommClass_self LinearMap.ext
rightComm_symm 📖	mathematical	—	LinearEquiv.symm TensorProduct addCommMonoid instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids rightComm	—	RingHomInvPair.ids
rightComm_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike rightComm tmul	—	RingHomInvPair.ids
tensorTensorTensorAssoc_symm_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm tensorTensorTensorAssoc tmul	—	RingHomInvPair.ids
tensorTensorTensorAssoc_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike tensorTensorTensorAssoc tmul	—	RingHomInvPair.ids
tensorTensorTensorComm_comp_map 📖	mathematical	—	LinearMap.comp TensorProduct addCommMonoid instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids tensorTensorTensorComm map	—	ext_fourfold' RingHomCompTriple.ids RingHomInvPair.ids
tensorTensorTensorComm_symm 📖	mathematical	—	LinearEquiv.symm TensorProduct addCommMonoid instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids tensorTensorTensorComm	—	RingHomInvPair.ids
tensorTensorTensorComm_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike tensorTensorTensorComm tmul	—	RingHomInvPair.ids
tensorTensorTensorComm_trans_tensorTensorTensorComm 📖	mathematical	—	LinearEquiv.trans TensorProduct addCommMonoid instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids tensorTensorTensorComm LinearEquiv.refl	—	RingHomInvPair.ids RingHomCompTriple.ids tensorTensorTensorComm_symm LinearEquiv.symm_trans_self
toLinearMap_symm_lid 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid instModule LinearEquiv.symm lid DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid LinearMap.instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids
toLinearMap_symm_rid 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid instModule LinearEquiv.symm rid DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_left smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.instFunLike LinearMap.flip AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids

---

← Back to Index