Maps

📁 Source: Mathlib/RingTheory/TensorProduct/Maps.lean

Statistics

Metric	Count
Definitions algEquivOfLinearEquivTensorProduct, algEquivOfLinearEquivTripleTensorProduct, algHomOfLinearMapTensorProduct, assoc, cancelBaseChange, comm, commRight, equivOfCompatibleSMul, lTensor, leftComm, lid, lidOfCompatibleSMul, liftEquiv, lmul', lmul'', lmulEquiv, map, mapOfCompatibleSMul, mapOfCompatibleSMul', productLeftAlgHom, productMap, rTensor, rid, tensorTensorTensorComm, tensorProduct, tensorProductEnd, lTensorAlgHom, rTensorAlgHom, endTensorEndAlgHom, baseChange	30
Theorems commRight_symm_tmul, adjoin_tmul_eq_top, algEquivOfLinearEquivTensorProduct_apply, algEquivOfLinearEquivTripleTensorProduct_apply, algHomOfLinearMapTensorProduct_apply, assoc_symm_tmul, assoc_tmul, assoc_toLinearEquiv, cancelBaseChange_symm_tmul, cancelBaseChange_tmul, commRight_tmul, comm_comp_includeLeft, comm_comp_includeRight, comm_comp_map, comm_comp_map_apply, comm_symm, comm_symm_tmul, comm_tmul, comm_toLinearEquiv, congr_apply, congr_refl, congr_symm, congr_symm_apply, congr_toLinearEquiv, congr_trans, includeLeft_bijective, includeRight_bijective, instCompatibleSMulRat, leftComm_symm_tmul, leftComm_tmul, leftComm_toLinearEquiv, lidOfCompatibleSMul_tmul, lid_symm_apply, lid_tmul, lid_toLinearEquiv, liftEquiv_apply, liftEquiv_symm_apply_coe, lift_comp_includeLeft, lift_comp_includeRight, lift_comp_includeRight', lift_includeLeft_includeRight, lift_tmul, lmul''_eq_lid_comp_mapOfCompatibleSMul, lmul'_apply_tmul, lmul'_comp_includeLeft, lmul'_comp_includeRight, lmul'_comp_map, lmul'_toLinearMap, lmulEquiv_eq_lidOfCompatibleSMul, mapOfCompatibleSMul_surjective, mapOfCompatibleSMul_tmul, map_bijective, map_comp, map_comp_id, map_comp_includeLeft, map_comp_includeRight, map_id, map_id_comp, map_range, map_restrictScalars_comp_includeRight, map_tmul, productMap_apply_tmul, productMap_eq_comp_map, productMap_left, productMap_left_apply, productMap_range, productMap_right, productMap_right_apply, rid_symm_apply, rid_tmul, rid_toLinearEquiv, tensorTensorTensorComm_symm, tensorTensorTensorComm_symm_tmul, tensorTensorTensorComm_tmul, tensorTensorTensorComm_toLinearEquiv, tmul_one_eq_one_tmul, toLinearEquiv_tensorTensorTensorComm, toLinearMap_map, map_mul_of_map_mul_tmul, tensorProductEnd_apply, tensorProduct_apply, lTensorAlgHom_apply_apply, rTensorAlgHom_apply_apply, endTensorEndAlgHom_apply, tmul_mem_baseChange	85
Total	115

Algebra.TensorProduct

Definitions

Name	Category	Theorems
algEquivOfLinearEquivTensorProduct 📖	CompOp	1 math math: algEquivOfLinearEquivTensorProduct_apply
algEquivOfLinearEquivTripleTensorProduct 📖	CompOp	1 math math: algEquivOfLinearEquivTripleTensorProduct_apply
algHomOfLinearMapTensorProduct 📖	CompOp	1 math math: algHomOfLinearMapTensorProduct_apply
assoc 📖	CompOp	8 math math: AlgCat.hom_inv_associator, assoc_tmul, AlgCat.hom_hom_associator, assoc_toLinearEquiv, assoc_symm_tmul, CommAlgCat.associator_inv_hom, CommAlgCat.associator_hom_hom, Bialgebra.TensorProduct.assoc_toAlgEquiv
cancelBaseChange 📖	CompOp	2 math math: cancelBaseChange_tmul, cancelBaseChange_symm_tmul
comm 📖	CompOp	13 math math: Subalgebra.mulMap_comm, CommAlgCat.braiding_hom_hom, comm_comp_map_apply, Subalgebra.comm_trans_rTensorBot, comm_comp_includeRight, comm_comp_includeLeft, CommAlgCat.braiding_inv_hom, comm_symm_tmul, comm_tmul, Subalgebra.comm_trans_lTensorBot, comm_comp_map, comm_toLinearEquiv, comm_symm
commRight 📖	CompOp	2 math math: commRight_tmul, Algebra.TensorProduct.commRight_symm_tmul
equivOfCompatibleSMul 📖	CompOp	—
lTensor 📖	CompOp	—
leftComm 📖	CompOp	3 math math: leftComm_tmul, leftComm_toLinearEquiv, leftComm_symm_tmul
lid 📖	CompOp	7 math math: lid_tmul, AlgCat.hom_inv_leftUnitor, AlgCat.hom_hom_leftUnitor, Bialgebra.TensorProduct.lid_toAlgEquiv, lmul''_eq_lid_comp_mapOfCompatibleSMul, lid_toLinearEquiv, lid_symm_apply
lidOfCompatibleSMul 📖	CompOp	2 math math: lmulEquiv_eq_lidOfCompatibleSMul, lidOfCompatibleSMul_tmul
liftEquiv 📖	CompOp	2 math math: liftEquiv_apply, liftEquiv_symm_apply_coe
lmul' 📖	CompOp	13 math math: Algebra.FormallyUnramified.lmul_elem, AlgebraicGeometry.diagonal_SpecMap, Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul, KaehlerDifferential.End_equiv_aux, lmul'_apply_tmul, lmul'_comp_map, productMap_eq_comp_map, lmul'_comp_includeRight, Derivation.tensorProductTo_mul, lmul'_comp_includeLeft, AlgebraicGeometry.diagonal_Spec_map, lmul'_toLinearMap, Algebra.FormallyUnramified.iff_exists_tensorProduct
lmul'' 📖	CompOp	1 math math: lmul''_eq_lid_comp_mapOfCompatibleSMul
lmulEquiv 📖	CompOp	1 math math: lmulEquiv_eq_lidOfCompatibleSMul
map 📖	CompOp	54 math math: CommRingCat.tensorProd_map_right, Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_right, Bialgebra.TensorProduct.map_toAlgHom, congr_symm_apply, map_comp, Subalgebra.centralizer_coe_map_includeLeft_eq_center_tensorProduct, Bialgebra.TensorProduct.counitAlgHom_def, comm_comp_map_apply, Subalgebra.mulMap_map_comp_eq, map_tmul, Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap, CliffordAlgebra.toBaseChange_comp_involute, Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap, Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProduct, Bialgebra.TensorProduct.comulAlgHom_def, map_ker, AlgHom.coe_tensorEqualizer, RingHom.SurjectiveOnStalks.tensorProductMap, Algebra.FiniteType.baseChangeAux_surj, lmul'_comp_map, Subalgebra.centralizer_coe_map_includeRight_eq_center_tensorProduct, map_id, congr_apply, productMap_eq_comp_map, map_comp_id, CommAlgCat.tensorHom_hom, Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_left, AlgCat.hom_whiskerLeft, map_surjective, AlgHom.tensorEqualizerEquiv_apply, CommAlgCat.whiskerLeft_hom, CommAlgCat.whiskerRight_hom, CliffordAlgebra.toBaseChange_comp_reverseOp, map_range, map_comp_includeRight, algEquivIncludeRange_toAlgHom, BialgHomClass.map_comp_comulAlgHom, RingHom.Finite.tensorProductMap, Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct, lTensor_ker, PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable, comm_comp_map, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, map_restrictScalars_comp_includeRight, Subalgebra.centralizer_coe_image_includeLeft_eq_center_tensorProduct, AlgCat.hom_tensorHom, toLinearMap_map, map_id_comp, AlgCat.hom_whiskerRight, map_bijective, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, rTensor_ker, map_comp_includeLeft, Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct
mapOfCompatibleSMul 📖	CompOp	2 math math: mapOfCompatibleSMul_surjective, mapOfCompatibleSMul_tmul
mapOfCompatibleSMul' 📖	CompOp	1 math math: lmul''_eq_lid_comp_mapOfCompatibleSMul
productLeftAlgHom 📖	CompOp	—
productMap 📖	CompOp	7 math math: productMap_left_apply, productMap_left, productMap_apply_tmul, productMap_range, productMap_eq_comp_map, productMap_right_apply, productMap_right
rTensor 📖	CompOp	—
rid 📖	CompOp	9 math math: AlgCat.hom_inv_rightUnitor, Bialgebra.TensorProduct.counitAlgHom_def, Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap, AlgCat.hom_hom_rightUnitor, Bialgebra.TensorProduct.rid_toAlgEquiv, rid_tmul, Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply, rid_toLinearEquiv, rid_symm_apply
tensorTensorTensorComm 📖	CompOp	7 math math: tensorTensorTensorComm_symm, Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap, tensorTensorTensorComm_symm_tmul, Bialgebra.TensorProduct.comulAlgHom_def, toLinearEquiv_tensorTensorTensorComm, tensorTensorTensorComm_toLinearEquiv, tensorTensorTensorComm_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_tmul_eq_top 📖	mathematical	—	Algebra.adjoin TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra setOf TensorProduct.tmul Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_le_iff LE.le.trans TensorProduct.span_tmul_eq_top Algebra.span_le_adjoin
algEquivOfLinearEquivTensorProduct_apply 📖	mathematical	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	AlgEquiv instSemiring leftAlgebra AlgEquiv.instFunLike algEquivOfLinearEquivTensorProduct	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass
algEquivOfLinearEquivTripleTensorProduct_apply 📖	mathematical	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike LinearEquiv.instEquivLike TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	AlgEquiv instSemiring instAlgebra AlgEquiv.instFunLike algEquivOfLinearEquivTripleTensorProduct	—	RingHomInvPair.ids
algHomOfLinearMapTensorProduct_apply 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass LinearMap.instFunLike TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	AlgHom instSemiring leftAlgebra AlgHom.funLike algHomOfLinearMapTensorProduct	—	IsScalarTower.to_smulCommClass
assoc_symm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' instSemiring leftAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AlgEquiv.instFunLike AlgEquiv.symm assoc TensorProduct.tmul	—	IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass TensorProduct.smulCommClass_left
assoc_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass instSemiring leftAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AlgEquiv.instFunLike assoc TensorProduct.tmul	—	IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' TensorProduct.smulCommClass_left
assoc_toLinearEquiv 📖	mathematical	—	AlgEquiv.toLinearEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass instSemiring leftAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction assoc TensorProduct.AlgebraTensorModule.assoc	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass TensorProduct.smulCommClass_left
cancelBaseChange_symm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass instSemiring leftAlgebra Algebra.id IsScalarTower.to_smulCommClass AlgEquiv.instFunLike AlgEquiv.symm cancelBaseChange TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul IsScalarTower.to_smulCommClass
cancelBaseChange_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass instSemiring leftAlgebra Algebra.id IsScalarTower.to_smulCommClass AlgEquiv.instFunLike cancelBaseChange TensorProduct.tmul Algebra.toSMul	—	TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul IsScalarTower.to_smulCommClass
commRight_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instSemiring leftAlgebra Algebra.id Algebra.to_smulCommClass rightAlgebra AlgEquiv.instFunLike commRight TensorProduct.tmul	—	Algebra.to_smulCommClass
comm_comp_includeLeft 📖	mathematical	—	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra AlgHomClass.toAlgHom AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass comm includeLeft includeRight	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
comm_comp_includeRight 📖	mathematical	—	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra AlgHomClass.toAlgHom AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass comm includeRight includeLeft	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
comm_comp_map 📖	mathematical	—	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction instAlgebra AlgHomClass.toAlgHom AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass comm map AlgEquiv.toAlgHom	—	ext IsScalarTower.left TensorProduct.isScalarTower IsScalarTower.to_smulCommClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgHom.ext TensorProduct.isScalarTower_left
comm_comp_map_apply 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra AlgEquiv.instFunLike comm AlgHom leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AlgHom.funLike map	—	IsScalarTower.to_smulCommClass IsScalarTower.left AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass comm_comp_map
comm_symm 📖	mathematical	—	AlgEquiv.symm TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra comm	—	AlgEquiv.ext
comm_symm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra AlgEquiv.instFunLike AlgEquiv.symm comm TensorProduct.tmul	—	—
comm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra AlgEquiv.instFunLike comm TensorProduct.tmul	—	—
comm_toLinearEquiv 📖	mathematical	—	AlgEquiv.toLinearEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra comm TensorProduct.comm	—	RingHomInvPair.ids
congr_apply 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring AlgEquiv.instFunLike congr AlgHom AlgHom.funLike map AlgHomClass.toAlgHom AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	—	IsScalarTower.to_smulCommClass
congr_refl 📖	mathematical	—	congr AlgEquiv.refl TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring	—	AlgEquiv.coe_algHom_injective IsScalarTower.to_smulCommClass map_id
congr_symm 📖	mathematical	—	congr AlgEquiv.symm TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring	—	IsScalarTower.to_smulCommClass
congr_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring AlgEquiv.instFunLike AlgEquiv.symm congr AlgHom AlgHom.funLike map AlgHomClass.toAlgHom AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	—	IsScalarTower.to_smulCommClass
congr_toLinearEquiv 📖	mathematical	—	AlgEquiv.toLinearEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring congr TensorProduct.AlgebraTensorModule.congr	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass
congr_trans 📖	mathematical	—	congr AlgEquiv.trans TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring	—	AlgEquiv.coe_algHom_injective IsScalarTower.to_smulCommClass map_comp
includeLeft_bijective 📖	mathematical	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule AlgHom instSemiring leftAlgebra IsScalarTower.to_smulCommClass AlgHom.funLike includeLeft	—	IsScalarTower.to_smulCommClass ext TensorProduct.isScalarTower_left AlgHom.ext one_smul map_comp_includeLeft Algebra.ext_id Function.Bijective.of_comp_iff AlgEquiv.bijective IsScalarTower.left DFunLike.coe_fn_eq map_bijective Function.bijective_id
includeRight_bijective 📖	mathematical	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule AlgHom instSemiring instAlgebra AlgHom.funLike includeRight	—	Function.Bijective.of_comp_iff' AlgEquiv.bijective includeLeft_bijective IsScalarTower.left
instCompatibleSMulRat 📖	mathematical	—	TensorProduct.CompatibleSMul Rat.monoid AddCommGroup.toAddCommMonoid Module.toDistribMulAction Rat.semiring	—	IsAddTorsionFree.of_module_rat SMulCommClass.rat' AddMonoid.nat_smulCommClass' TensorProduct.smul_tmul' TensorProduct.tmul_smul TensorProduct.CompatibleSMul.isScalarTower AddCommMonoid.nat_isScalarTower smul_assoc nsmul_eq_mul Rat.den_mul_eq_num Int.cast_smul_eq_zsmul TensorProduct.smul_tmul TensorProduct.CompatibleSMul.int smul_right_injective IsAddTorsionFree.to_isTorsionFree_nat Nat.instIsCancelMulZero
leftComm_symm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.instModule instSemiring instAlgebra AlgEquiv.instFunLike AlgEquiv.symm leftComm TensorProduct.tmul	—	—
leftComm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.instModule instSemiring instAlgebra AlgEquiv.instFunLike leftComm TensorProduct.tmul	—	—
leftComm_toLinearEquiv 📖	mathematical	—	SemilinearEquivClass.semilinearEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.instModule AlgEquiv instSemiring instAlgebra CommSemiring.toSemiring RingHom.id RingHomInvPair.ids AlgEquiv.instEquivLike AlgEquivClass.toLinearEquivClass AlgEquiv.instAlgEquivClass leftComm TensorProduct.leftComm	—	LinearEquiv.toLinearMap_injective RingHomInvPair.ids AlgEquivClass.toLinearEquivClass AlgEquiv.instAlgEquivClass TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.left TensorProduct.isScalarTower LinearMap.ext IsScalarTower.to_smulCommClass
lidOfCompatibleSMul_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instSemiring leftAlgebra Algebra.id Algebra.to_smulCommClass AlgEquiv.instFunLike lidOfCompatibleSMul TensorProduct.tmul Algebra.toSMul	—	Algebra.to_smulCommClass
lid_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule instSemiring Algebra.id instAlgebra AlgEquiv.instFunLike AlgEquiv.symm lid TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
lid_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule instSemiring Algebra.id instAlgebra AlgEquiv.instFunLike lid TensorProduct.tmul Algebra.toSMul	—	—
lid_toLinearEquiv 📖	mathematical	—	AlgEquiv.toLinearEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule instSemiring Algebra.id instAlgebra lid TensorProduct.lid	—	RingHomInvPair.ids
liftEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv AlgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring EquivLike.toFunLike Equiv.instEquivLike liftEquiv lift	—	IsScalarTower.to_smulCommClass
liftEquiv_symm_apply_coe 📖	mathematical	—	AlgHom DFunLike.coe Equiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring EquivLike.toFunLike Equiv.instEquivLike Equiv.symm liftEquiv AlgHom.comp includeLeft instAlgebra AlgHom.restrictScalars includeRight	—	IsScalarTower.to_smulCommClass
lift_comp_includeLeft 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe AlgHom AlgHom.funLike	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring lift includeLeft	—	AlgHom.ext IsScalarTower.to_smulCommClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass mul_one
lift_comp_includeRight 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe AlgHom AlgHom.funLike	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule instSemiring instAlgebra AlgHom.restrictScalars leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring TensorProduct.isScalarTower_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul lift includeRight	—	AlgHom.ext IsScalarTower.to_smulCommClass TensorProduct.isScalarTower_left map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass one_mul
lift_comp_includeRight' 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe AlgHom AlgHom.funLike	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction lift includeRight	—	AlgHom.ext IsScalarTower.to_smulCommClass IsScalarTower.left map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass one_mul
lift_includeLeft_includeRight 📖	mathematical	—	lift TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring instAlgebra TensorProduct.isScalarTower_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul includeLeft includeRight Commute.tmul Algebra.to_smulCommClass IsScalarTower.right AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Commute.one_right MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Commute.one_left AlgHom.id	—	ext IsScalarTower.to_smulCommClass TensorProduct.isScalarTower_left Commute.tmul Algebra.to_smulCommClass IsScalarTower.right Commute.one_right Commute.one_left AlgHom.ext mul_one one_mul
lift_tmul 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe AlgHom AlgHom.funLike	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring lift TensorProduct.tmul	—	IsScalarTower.to_smulCommClass
lmul''_eq_lid_comp_mapOfCompatibleSMul 📖	mathematical	—	lmul'' AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Semiring.toModule Algebra.id instSemiring leftAlgebra SMulCommClass.symm Algebra.toSMul IsScalarTower.to_smulCommClass' IsScalarTower.right instAlgebra AlgEquiv.toAlgHom lid mapOfCompatibleSMul' TensorProduct.CompatibleSMul.isScalarTower MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	ext IsScalarTower.right SMulCommClass.symm IsScalarTower.to_smulCommClass' TensorProduct.CompatibleSMul.isScalarTower Algebra.ext_id IsScalarTower.to_smulCommClass AlgHom.ext TensorProduct.isScalarTower_left
lmul'_apply_tmul 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instSemiring instAlgebra AlgHom.funLike lmul' TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
lmul'_comp_includeLeft 📖	mathematical	—	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instSemiring instAlgebra lmul' includeLeft AlgHom.id	—	AlgHom.ext mul_one
lmul'_comp_includeRight 📖	mathematical	—	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instSemiring instAlgebra lmul' includeRight AlgHom.id	—	AlgHom.ext one_mul
lmul'_comp_map 📖	mathematical	—	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule CommSemiring.toSemiring instSemiring leftAlgebra IsScalarTower.to_smulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction instAlgebra lmul' map lift Commute.all NonUnitalNonAssocCommSemiring.toCommMagma NonUnitalCommSemiring.toNonUnitalNonAssocCommSemiring CommSemiring.toNonUnitalCommSemiring DFunLike.coe AlgHom AlgHom.funLike	—	ext IsScalarTower.left IsScalarTower.to_smulCommClass Commute.all AlgHom.ext TensorProduct.isScalarTower_left
lmul'_toLinearMap 📖	mathematical	—	AlgHom.toLinearMap TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instSemiring instAlgebra lmul' LinearMap.mul' Algebra.to_smulCommClass IsScalarTower.right	—	—
lmulEquiv_eq_lidOfCompatibleSMul 📖	mathematical	—	lmulEquiv lidOfCompatibleSMul CommSemiring.toSemiring Algebra.id TensorProduct.CompatibleSMul.isScalarTower MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction Algebra.toModule Semiring.toModule Algebra.toSMul IsScalarTower.right	—	AlgEquiv.coe_algHom_injective Algebra.to_smulCommClass TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.right ext AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Algebra.ext_id IsScalarTower.to_smulCommClass AlgHom.ext TensorProduct.isScalarTower_left
mapOfCompatibleSMul_surjective 📖	mathematical	—	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule DFunLike.coe AlgHom instSemiring instAlgebra leftAlgebra AlgHom.funLike mapOfCompatibleSMul	—	TensorProduct.mapOfCompatibleSMul_surjective
mapOfCompatibleSMul_tmul 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra leftAlgebra AlgHom.funLike mapOfCompatibleSMul TensorProduct.tmul	—	—
map_bijective 📖	mathematical	Function.Bijective DFunLike.coe AlgHom AlgHom.funLike	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction map	—	TensorProduct.map_bijective
map_comp 📖	mathematical	—	map AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring	—	ext IsScalarTower.to_smulCommClass TensorProduct.isScalarTower_left AlgHom.ext
map_comp_id 📖	mathematical	—	map AlgHom.comp AlgHom.id TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring	—	ext IsScalarTower.to_smulCommClass TensorProduct.isScalarTower_left AlgHom.ext
map_comp_includeLeft 📖	mathematical	—	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring map includeLeft	—	AlgHom.ext IsScalarTower.to_smulCommClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
map_comp_includeRight 📖	mathematical	—	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction map includeRight instAlgebra	—	map_restrictScalars_comp_includeRight IsScalarTower.left
map_id 📖	mathematical	—	map AlgHom.id TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring	—	ext IsScalarTower.to_smulCommClass TensorProduct.isScalarTower_left AlgHom.ext
map_id_comp 📖	mathematical	—	map AlgHom.id AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring	—	ext IsScalarTower.to_smulCommClass TensorProduct.isScalarTower_left AlgHom.ext
map_range 📖	mathematical	—	AlgHom.range TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction map Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra AlgHom.comp includeLeft instAlgebra includeRight	—	le_antisymm IsScalarTower.to_smulCommClass IsScalarTower.left Algebra.map_top adjoin_tmul_eq_top Algebra.adjoin_image Algebra.adjoin_le_iff map_tmul mul_one one_mul Algebra.to_smulCommClass IsScalarTower.right tmul_mul_tmul Algebra.mul_mem_sup AlgHom.mem_range_self map_comp_includeLeft map_comp_includeRight sup_le AlgHom.range_comp_le_range
map_restrictScalars_comp_includeRight 📖	mathematical	—	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra AlgHom.restrictScalars leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring TensorProduct.isScalarTower_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul map includeRight	—	AlgHom.ext IsScalarTower.to_smulCommClass TensorProduct.isScalarTower_left map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
map_tmul 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring AlgHom.funLike map TensorProduct.tmul	—	IsScalarTower.to_smulCommClass
productMap_apply_tmul 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring CommSemiring.toSemiring instAlgebra AlgHom.funLike productMap TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
productMap_eq_comp_map 📖	mathematical	—	productMap AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule CommSemiring.toSemiring instSemiring leftAlgebra IsScalarTower.to_smulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction instAlgebra lmul' map	—	ext IsScalarTower.left IsScalarTower.to_smulCommClass AlgHom.ext TensorProduct.isScalarTower_left
productMap_left 📖	mathematical	—	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring CommSemiring.toSemiring instAlgebra productMap includeLeft	—	lift_comp_includeLeft Commute.all
productMap_left_apply 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring CommSemiring.toSemiring instAlgebra AlgHom.funLike productMap TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass mul_one
productMap_range 📖	mathematical	—	AlgHom.range TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring instAlgebra CommSemiring.toSemiring productMap Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra	—	IsScalarTower.to_smulCommClass IsScalarTower.left productMap_eq_comp_map AlgHom.range_comp map_range Algebra.map_sup AlgHom.comp_assoc lmul'_comp_includeLeft lmul'_comp_includeRight AlgHom.id_comp
productMap_right 📖	mathematical	—	AlgHom.comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring CommSemiring.toSemiring instAlgebra productMap includeRight	—	lift_comp_includeRight IsScalarTower.left Commute.all
productMap_right_apply 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring CommSemiring.toSemiring instAlgebra AlgHom.funLike productMap TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass one_mul
rid_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Semiring.toModule instSemiring Algebra.id leftAlgebra IsScalarTower.to_smulCommClass AlgEquiv.instFunLike AlgEquiv.symm rid TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	IsScalarTower.to_smulCommClass
rid_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Semiring.toModule instSemiring Algebra.id leftAlgebra IsScalarTower.to_smulCommClass AlgEquiv.instFunLike rid TensorProduct.tmul Algebra.toSMul	—	IsScalarTower.to_smulCommClass
rid_toLinearEquiv 📖	mathematical	—	AlgEquiv.toLinearEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Semiring.toModule instSemiring Algebra.id leftAlgebra IsScalarTower.to_smulCommClass rid TensorProduct.AlgebraTensorModule.rid	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass
tensorTensorTensorComm_symm 📖	mathematical	—	AlgEquiv.symm TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass instSemiring leftAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction tensorTensorTensorComm	—	IsScalarTower.to_smulCommClass TensorProduct.smulCommClass_left
tensorTensorTensorComm_symm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass instSemiring leftAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AlgEquiv.instFunLike AlgEquiv.symm tensorTensorTensorComm TensorProduct.tmul	—	IsScalarTower.to_smulCommClass TensorProduct.smulCommClass_left
tensorTensorTensorComm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass instSemiring leftAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AlgEquiv.instFunLike tensorTensorTensorComm TensorProduct.tmul	—	IsScalarTower.to_smulCommClass TensorProduct.smulCommClass_left
tensorTensorTensorComm_toLinearEquiv 📖	mathematical	—	AlgEquiv.toLinearEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass instSemiring leftAlgebra TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction tensorTensorTensorComm TensorProduct.AlgebraTensorModule.tensorTensorTensorComm	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass TensorProduct.smulCommClass_left
tmul_one_eq_one_tmul 📖	mathematical	—	TensorProduct.tmul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Algebra.algebraMap_eq_smul_one TensorProduct.smul_tmul TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left
toLinearEquiv_tensorTensorTensorComm 📖	mathematical	—	AlgEquiv.toLinearEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring leftAlgebra TensorProduct.smulCommClass_left tensorTensorTensorComm TensorProduct.tensorTensorTensorComm	—	RingHomInvPair.ids smulCommClass_self IsScalarTower.to_smulCommClass IsScalarTower.left TensorProduct.smulCommClass_left
toLinearMap_map 📖	mathematical	—	AlgHom.toLinearMap TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSemiring leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring map TensorProduct.AlgebraTensorModule.map	—	IsScalarTower.to_smulCommClass

Algebra.TensorProduct.Algebra.TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commRight_symm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.rightAlgebra Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass AlgEquiv.instFunLike AlgEquiv.symm Algebra.TensorProduct.commRight TensorProduct.tmul	—	Algebra.to_smulCommClass

LinearMap

Definitions

Name	Category	Theorems
tensorProduct 📖	CompOp	4 math math: polyCharpoly_baseChange, polyCharpolyAux_baseChange, polyCharpolyAux_map_aeval, tensorProduct_apply
tensorProductEnd 📖	CompOp	1 math math: tensorProductEnd_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mul_of_map_mul_tmul 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass instFunLike TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	Algebra.TensorProduct.instMul Algebra.to_smulCommClass IsScalarTower.right	—	IsScalarTower.to_smulCommClass Algebra.to_smulCommClass IsScalarTower.right smulCommClass_self IsScalarTower.left RingHomCompTriple.ids map_mul_iff TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.to_smulCommClass' RestrictScalars.isScalarTower instIsScalarTower ext
tensorProductEnd_apply 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct Module.End CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring addCommMonoid RingHom.id Algebra.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Algebra.TensorProduct.instSemiring Module.End.instSemiring Module.End.instAlgebra Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.TensorProduct.leftAlgebra TensorProduct.smulCommClass_left TensorProduct.isScalarTower_left IsScalarTower.right AlgHom.funLike tensorProductEnd AddMonoidHom LinearMap AddZeroClass.toAddZero TensorProduct.addZeroClass AddMonoid.toAddZeroClass AddMonoidHom.instFunLike TensorProduct.liftAux TensorProduct.instModule restrictScalars IsScalarTower.to_smulCommClass AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instSMul DistribMulAction.toDistribSMul instDistribMulAction TensorProduct.leftDistribMulAction baseChangeHom	—	smulCommClass_self Algebra.to_smulCommClass IsScalarTower.left TensorProduct.smulCommClass_left TensorProduct.isScalarTower_left IsScalarTower.right
tensorProduct_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring addCommMonoid Algebra.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.id instFunLike tensorProduct AddMonoidHom AddZeroClass.toAddZero TensorProduct.addZeroClass AddMonoid.toAddZeroClass AddMonoidHom.instFunLike TensorProduct.liftAux TensorProduct.instModule restrictScalars IsScalarTower.to_smulCommClass AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instSMul DistribMulAction.toDistribSMul instDistribMulAction TensorProduct.leftDistribMulAction baseChangeHom	—	smulCommClass_self Algebra.to_smulCommClass TensorProduct.smulCommClass_left

Module

Definitions

Name	Category	Theorems
endTensorEndAlgHom 📖	CompOp	1 math math: endTensorEndAlgHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
endTensorEndAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct End CommSemiring.toSemiring LinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.module IsScalarTower.to_smulCommClass' smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass Algebra.TensorProduct.instSemiring End.instSemiring End.instAlgebra Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.TensorProduct.leftAlgebra LinearMap.instSMulCommClass DistribMulAction.toDistribSMul TensorProduct.smulCommClass_left TensorProduct.isScalarTower_left AlgHom.funLike endTensorEndAlgHom TensorProduct.tmul TensorProduct.AlgebraTensorModule.map	—	IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' smulCommClass_self IsScalarTower.left LinearMap.instSMulCommClass TensorProduct.smulCommClass_left TensorProduct.isScalarTower_left

Module.End

Definitions

Name	Category	Theorems
lTensorAlgHom 📖	CompOp	1 math math: lTensorAlgHom_apply_apply
rTensorAlgHom 📖	CompOp	1 math math: rTensorAlgHom_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lTensorAlgHom_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike AlgHom Module.End instSemiring instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero TensorProduct.smulCommClass_left TensorProduct.isScalarTower AlgHom.funLike lTensorAlgHom AddMonoidHom AddZeroClass.toAddZero TensorProduct.addZeroClass AddMonoid.toAddZeroClass AddMonoidHom.instFunLike TensorProduct.liftAux LinearMap.compl₂	—	smulCommClass_self IsScalarTower.left TensorProduct.smulCommClass_left TensorProduct.isScalarTower
rTensorAlgHom_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike AlgHom Module.End instSemiring instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero TensorProduct.smulCommClass_left TensorProduct.isScalarTower AlgHom.funLike rTensorAlgHom AddMonoidHom AddZeroClass.toAddZero TensorProduct.addZeroClass AddMonoid.toAddZeroClass AddMonoidHom.instFunLike TensorProduct.liftAux LinearMap.comp LinearMap.addCommMonoid LinearMap.module	—	LinearMap.comp.congr_simp LinearMap.compl₂_id

Subalgebra

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	2 math math: exists_fg_and_mem_baseChange, tmul_mem_baseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tmul_mem_baseChange 📖	mathematical	Subalgebra SetLike.instMembership instSetLike	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass baseChange TensorProduct.tmul	—	—

---

← Back to Index