Basic

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

Statistics

Metric	Count
Definitions aux, addCommGroup, comm, curry, equivOfCompatibleSMul, lcurry, equiv, liftAddHom, liftAux, mapOfCompatibleSMul, mapOfCompatibleSMul', neg, uncurry	13
Theorems int, unit, comm_comm, comm_comp_comm, comm_comp_comm_assoc, comm_symm, comm_symm_tmul, comm_tmul, comm_trans_comm, curry_apply, curry_injective, ext, ext', ext_fourfold, ext_fourfold', ext_fourfold'', ext_iff, ext_threefold, ext_threefold', lcurry_apply, equiv_apply, equiv_symm_apply, tmul, tmul', unique, liftAddHom_tmul, smul, smulₛₗ, liftAux_tmul, lift_comp_comm_eq, lift_compr₂, lift_compr₂ₛₗ, lift_mk, lift_mk_compr₂, lift_mk_compr₂ₛₗ, mapOfCompatibleSMul_surjective, mapOfCompatibleSMul_tmul, neg_add_cancel, neg_tmul, sub_tmul, tmul_neg, tmul_sub, uncurry_apply	43
Total	56

TensorProduct

Definitions

Name	Category	Theorems
addCommGroup 📖	CompOp	166 math math: Representation.repOfTprodIso_inv_apply, CliffordAlgebra.toBaseChange_reverse, lTensor.inverse_comp_lTensor, AlternatingMap.domCoprod.summand_mk'', LieModule.liftLie_apply, Rep.MonoidalClosed.linearHomEquiv_symm_hom, LieSubmodule.lowerCentralSeries_tensor_eq_baseChange, LinearMap.lTensor_sub, Representation.repOfTprodIso_apply, Rep.coindToInd_of_support_subset_orbit, Representation.Coinvariants.mk_inv_tmul, Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single, lTensor.inverse_of_rightInverse_comp_lTensor, CliffordAlgebra.equivBaseChange_symm_apply, Module.FaithfullyFlat.instTensorProduct, quotientTensorQuotientEquiv_symm_apply_mk_tmul, CoalgCat.tensorObj_isAddCommGroup, Rep.finsuppToCoinvariantsTensorFree_single, Representation.Coinvariants.mk_tmul_inv, CharacterModule.curry_apply_apply, LinearMap.det_baseChange, LinearEquiv.det_baseChange, rTensor.inverse_of_rightInverse_apply, CliffordAlgebra.ofBaseChange_toBaseChange, QuadraticForm.polarBilin_baseChange, ModuleCat.ExtendRestrictScalarsAdj.Counit.map_hom_apply, tmul_sub, CliffordAlgebra.toBaseChange_comp_ofBaseChange, ModuleCat.MonoidalCategory.whiskerLeft_def, Rep.ihom_ev_app_hom, lTensor.inverse_of_rightInverse_apply, QuadraticForm.polarBilin_tmul, Module.Presentation.tensor_R, LinearMap.rTensor_sub, Module.comap_freeLocus_le, CliffordAlgebra.toBaseChange_comp_involute, ModuleCat.MonoidalCategory.tensorHom_def, quotientTensorEquiv_symm_apply_mk_tmul, QuadraticForm.tensorAssoc_toLinearEquiv, LinearMap.polyCharpoly_baseChange, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, Representation.coinvariantsTprodLeftRegularLEquiv_apply, CoalgCat.tensorHom_def, lTensor.inverse_apply, KaehlerDifferential.tensorKaehlerEquivBase_symm_apply, RingTheory.Sequence.IsWeaklyRegular.isWeaklyRegular_lTensor, Rep.coinvariantsTensorFreeLEquiv_apply, Module.rankAtStalk_baseChange, MultilinearMap.domCoprod_alternization_coe, LieModule.weight_vector_multiplication, CoalgCat.associator_def, CoalgCat.comul_def, ModuleCat.MonoidalCategory.rightUnitor_def, ModuleCat.MonoidalCategory.associator_def, Rep.indResAdjunction_counit_app_hom_hom, LinearMap.lTensor_neg, LieSubmodule.mem_baseChange_iff, QuadraticMap.associated_tmul, Rep.coindToInd_apply, MultilinearMap.domCoprod_alternization_eq, ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply, LinearMap.toMvPolynomial_baseChange, CoalgCat.whiskerRight_def, Algebra.Extension.CotangentSpace.map_sub_map, QuadraticForm.tmul_tensorAssoc_apply, LieModule.map_tmul, Rep.finsuppTensorRight_hom_hom, LieModule.instIsNilpotentTensor, LieModule.coe_liftLie_eq_lift_coe, Module.Relations.Solution.IsPresentation.tensor, Module.rankAtStalk_tensorProduct, ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, Module.rankAtStalk_tensorProduct_of_isScalarTower, CliffordAlgebra.ofBaseChange_tmul_ι, KaehlerDifferential.tensorKaehlerEquiv_left_inv, rTensor.inverse_of_rightInverse_comp_rTensor, Module.Presentation.tensor_G, CliffordAlgebra.ofBaseChangeAux_ι, quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, LieSubmodule.lie_baseChange, tensorQuotientEquiv_apply_mk_tmul, LieModule.toModuleHom_apply, rTensor.inverse_comp_rTensor, Module.Relations.Solution.tensor_var, QuadraticForm.tensorAssoc_symm_apply, CliffordAlgebra.toBaseChange_ofBaseChange, CharacterModule.homEquiv_symm_apply_apply_apply, RingTheory.Sequence.IsWeaklyRegular.isWeaklyRegular_rTensor, LinearMap.polyCharpolyAux_baseChange, LinearMap.baseChange_sub, LieSubmodule.tmul_mem_baseChange_of_mem, groupHomology.H1AddEquivOfIsTrivial_symm_apply, LieModule.lift_apply, LieModule.lie_tmul_right, CliffordAlgebra.toBaseChange_comp_reverseOp, groupHomology.H1ToTensorOfIsTrivial_H1π_single, LinearMap.baseChange_neg, sub_tmul, LinearMap.polyCharpolyAux_map_aeval, ModuleCat.MonoidalCategory.tensorObj_isAddCommGroup, ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul, Rep.finsuppTensorRight_inv_hom, LieModule.toEnd_baseChange, LieModule.toLinearMap_map, CharacterModule.dual_rTensor_conj_homEquiv, CoalgCat.whiskerLeft_def, MultilinearMap.domCoprod_alternization, quotientTensorEquiv_apply_tmul_mk, CliffordAlgebra.equivBaseChange_apply, Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply, groupHomology.H1AddEquivOfIsTrivial_apply, Rep.finsuppTensorLeft_inv_hom, Module.Presentation.tensor_relation, LinearEquiv.dilatransvection.baseChange, Rep.leftRegularTensorTrivialIsoFree_inv_hom, rTensor.inverse_apply, Rep.linearization_δ_hom, QuadraticForm.tensorAssoc_apply, Rep.finsuppTensorLeft_hom_hom, LieSubmodule.lieIdeal_oper_eq_tensor_map_range, ModuleCat.MonoidalCategory.leftUnitor_def, CliffordAlgebra.toBaseChange_involute, Rep.coinvariantsTensorMk_apply, Rep.indMap_hom, CharacterModule.uncurry_apply, Rep.homEquiv_symm_apply_hom, Representation.ind_mk, CoalgCat.rightUnitor_def, LinearEquiv.transvection.baseChange, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, CliffordAlgebra.ofBaseChange_tmul_one, gradedCommAux_lof_tmul, CoalgCat.tensorObj_instCoalgebra, CliffordAlgebra.toBaseChange_ι, LinearMap.rTensor_neg, LieAlgebra.ExtendScalars.instLieModule, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, LieModule.lieModule, QuadraticForm.tmul_comp_tensorAssoc, QuadraticForm.associated_tmul, Representation.ind_apply, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, LieSubmodule.coe_baseChange, SpecialLinearGroup.baseChange_apply_coe, CoalgCat.leftUnitor_def, CharacterModule.homEquiv_apply_apply, tensorQuotientEquiv_symm_apply_tmul_mk, ModuleCat.MonoidalCategory.whiskerRight_def, gradedComm_of_tmul_of, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, LieSubmodule.baseChange_top, QuadraticForm.associated_baseChange, CliffordAlgebra.ofBaseChange_comp_toBaseChange, Rep.leftRegularTensorTrivialIsoFree_hom_hom, LieAlgebra.rootSpaceProduct_tmul, LinearMap.charpoly_baseChange, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, ModuleCat.ihom_ev_app, Representation.IndV.hom_ext_iff, Rep.indResHomEquiv_symm_apply_hom, QuadraticModuleCat.hom_hom_associator, Rep.linearization_μ_hom, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, Module.Presentation.tensor_var, QuadraticModuleCat.hom_inv_associator, LieSubmodule.baseChange_bot
comm 📖	CompOp	52 math math: Submodule.comm_trans_lTensorOne, LinearMap.rTensor_comm, enorm_comm, map_comp_comm_eq, LinearMap.mul'_comp_comm, dualDistrib_apply_comm, comm_comm, Submodule.mulMap_comm, QuadraticForm.tmul_comp_tensorComm, LinearEquiv.comm_trans_lTensor_trans_comm_eq, LinearMap.lTensor_comp_comm, Pi.intrinsicStar_comul_commSemiring, Coalgebra.comm_comul, comm_trans_lid, Module.Invertible.tensorProductComm_eq_refl, LinearMap.intrinsicStar_mul', comm_symm, norm_comm, leftComm_def, toLinearEquiv_commIsometry, Submodule.comm_trans_rTensorOne, QuadraticForm.tmul_tensorComm_apply, LinearMap.comm_comp_lTensor_comp_comm_eq, Coalgebra.IsCocomm.comm_comp_comul, map_comm, QuadraticForm.tensorComm_toLinearEquiv, LinearMap.lTensor_comm, QuadraticForm.tensorComm_apply, LinearMap.rTensor_comp_comm, comm_trans_comm, inner_comm_comm, Submodule.mulMap_comm_of_commute, PointedCone.minTensorProduct_comm, PointedCone.maxTensorProduct_comm, commIsometry_apply, LinearEquiv.comm_trans_rTensor_trans_comm_eq, nnnorm_comm, comm_tmul, comm_comp_comm_assoc, comm_comp_comm, Submodule.mulMap_op, lift_comp_comm_eq, LinearMap.mul'_comm, Equiv.tensorProductComm_def, toMatrix_comm, comm_symm_tmul, LinearMap.comm_comp_rTensor_comp_comm_eq, Coalgebra.comm_comp_comul, Algebra.TensorProduct.comm_toLinearEquiv, rightComm_def, comm_trans_rid, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply
curry 📖	CompOp	9 math math: Rep.homEquiv_apply_hom, gradedMul_def, AlgebraTensorModule.restrictScalars_curry, Rep.MonoidalClosed.linearHomEquivComm_hom, curry_injective, Module.Invertible.bijective_curry, AlgebraTensorModule.curry_apply, curry_apply, Rep.MonoidalClosed.linearHomEquiv_hom
equivOfCompatibleSMul 📖	CompOp	—
lcurry 📖	CompOp	1 math math: lcurry_apply
liftAddHom 📖	CompOp	2 math math: liftAddHom_tmul, CharacterModule.uncurry_apply
liftAux 📖	CompOp	10 math math: liftAux_tmul, Module.Invertible.rTensorEquiv_apply_apply, LinearMap.tensorProductEnd_apply, Module.End.rTensorAlgHom_apply_apply, LinearMap.mul''_apply, Module.End.baseChangeHom_apply_apply, LinearMap.tensorProduct_apply, liftAux.smul, Module.End.lTensorAlgHom_apply_apply, liftAux.smulₛₗ
mapOfCompatibleSMul 📖	CompOp	2 math math: mapOfCompatibleSMul_surjective, mapOfCompatibleSMul_tmul
mapOfCompatibleSMul' 📖	CompOp	—
neg 📖	CompOp	4 math math: neg_tmul, neg_add_cancel, tmul_neg, MvPolynomial.universalFactorizationMapPresentation_jacobian
uncurry 📖	CompOp	6 math math: Rep.MonoidalClosed.linearHomEquiv_symm_hom, Rep.ihom_ev_app_hom, Rep.homEquiv_symm_apply_hom, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, ModuleCat.ihom_ev_app, uncurry_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm_comm 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike comm	—	RingHomInvPair.ids RingHomCompTriple.ids comm_trans_comm
comm_comp_comm 📖	mathematical	—	LinearMap.comp TensorProduct CommSemiring.toSemiring addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids comm LinearMap.id	—	RingHomCompTriple.ids RingHomInvPair.ids comm_trans_comm
comm_comp_comm_assoc 📖	mathematical	—	LinearMap.comp TensorProduct CommSemiring.toSemiring addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids comm	—	RingHomCompTriple.ids RingHomInvPair.ids LinearMap.comp_assoc comm_comp_comm RingHomCompTriple.right_ids LinearMap.id_comp
comm_symm 📖	mathematical	—	LinearEquiv.symm TensorProduct CommSemiring.toSemiring addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids comm	—	RingHomInvPair.ids
comm_symm_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm comm tmul	—	RingHomInvPair.ids
comm_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike comm tmul	—	RingHomInvPair.ids
comm_trans_comm 📖	mathematical	—	LinearEquiv.trans TensorProduct CommSemiring.toSemiring addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids comm LinearEquiv.refl	—	LinearEquiv.toLinearMap_injective RingHomInvPair.ids RingHomCompTriple.ids ext LinearMap.ext smulCommClass_self
curry_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction curry TensorProduct addCommMonoid instModule tmul	—	smulCommClass_self
curry_injective 📖	mathematical	—	LinearMap CommSemiring.toSemiring TensorProduct addCommMonoid instModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction curry	—	smulCommClass_self ext
ext 📖	—	LinearMap.compr₂ₛₗ TensorProduct addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHomCompTriple.ids	—	—	smulCommClass_self RingHomCompTriple.ids lift_mk_compr₂ₛₗ
ext' 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring TensorProduct addCommMonoid instModule LinearMap.instFunLike tmul	—	—	LinearMap.ext induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.map_add
ext_fourfold 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring TensorProduct addCommMonoid instModule LinearMap.instFunLike tmul	—	—	ext smulCommClass_self RingHomCompTriple.ids LinearMap.ext
ext_fourfold' 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring TensorProduct addCommMonoid instModule LinearMap.instFunLike tmul	—	—	ext smulCommClass_self RingHomCompTriple.ids LinearMap.ext
ext_fourfold'' 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring TensorProduct addCommMonoid instModule LinearMap.instFunLike tmul	—	—	ext smulCommClass_self RingHomCompTriple.ids LinearMap.ext
ext_iff 📖	mathematical	—	LinearMap.compr₂ₛₗ TensorProduct addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHomCompTriple.ids	—	smulCommClass_self RingHomCompTriple.ids ext
ext_threefold 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring TensorProduct addCommMonoid instModule LinearMap.instFunLike tmul	—	—	ext smulCommClass_self RingHomCompTriple.ids LinearMap.ext
ext_threefold' 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring TensorProduct addCommMonoid instModule LinearMap.instFunLike tmul	—	—	ext LinearMap.ext smulCommClass_self RingHomCompTriple.ids
lcurry_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id Semiring.toNonAssocSemiring TensorProduct addCommMonoid instModule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero lcurry tmul	—	smulCommClass_self LinearMap.instSMulCommClass
liftAddHom_tmul 📖	mathematical	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike AddMonoidHom.instAddCommMonoid SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	TensorProduct addZeroClass liftAddHom tmul	—	—
liftAux_tmul 📖	mathematical	—	DFunLike.coe AddMonoidHom TensorProduct AddZeroClass.toAddZero addZeroClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike liftAux tmul LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction	—	smulCommClass_self
lift_comp_comm_eq 📖	mathematical	—	LinearMap.comp TensorProduct CommSemiring.toSemiring addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lift LinearEquiv.toLinearMap RingHomInvPair.ids comm LinearMap.flip smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self ext RingHomCompTriple.ids RingHomInvPair.ids
lift_compr₂ 📖	mathematical	—	lift RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring LinearMap.compr₂ smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.comp TensorProduct addCommMonoid instModule RingHomCompTriple.ids	—	smulCommClass_self RingHomCompTriple.ids IsScalarTower.left lift.unique
lift_compr₂ₛₗ 📖	mathematical	—	lift LinearMap.compr₂ₛₗ LinearMap.comp TensorProduct CommSemiring.toSemiring addCommMonoid instModule	—	smulCommClass_self lift.unique
lift_mk 📖	mathematical	—	lift RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring TensorProduct addCommMonoid instModule LinearMap.id	—	lift.unique
lift_mk_compr₂ 📖	mathematical	—	lift RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring LinearMap.compr₂ TensorProduct addCommMonoid instModule smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Semiring.toModule IsScalarTower.left isScalarTower SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	smulCommClass_left smulCommClass_self IsScalarTower.left isScalarTower RingHomCompTriple.ids lift_compr₂ LinearMap.comp_id
lift_mk_compr₂ₛₗ 📖	mathematical	—	lift LinearMap.compr₂ₛₗ TensorProduct addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHomCompTriple.ids	—	RingHomCompTriple.ids lift_compr₂ₛₗ LinearMap.comp_id
mapOfCompatibleSMul_surjective 📖	mathematical	—	TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid instModule leftModule LinearMap.instFunLike mapOfCompatibleSMul	—	induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass mapOfCompatibleSMul_tmul map_add SemilinearMapClass.toAddHomClass
mapOfCompatibleSMul_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct addCommMonoid instModule leftModule LinearMap.instFunLike mapOfCompatibleSMul tmul	—	—
neg_add_cancel 📖	mathematical	—	TensorProduct AddCommGroup.toAddCommMonoid add neg zero	—	induction_on add_zero LinearMap.map_zero neg_add_cancel zero_tmul add_tmul map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Mathlib.Tactic.Abel.subst_into_add Mathlib.Tactic.Abel.term_atom Mathlib.Tactic.Abel.term_add_const zero_add Mathlib.Tactic.Abel.const_add_term
neg_tmul 📖	mathematical	—	tmul AddCommGroup.toAddCommMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid TensorProduct neg	—	—
sub_tmul 📖	mathematical	—	tmul AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup TensorProduct addCommGroup	—	LinearMap.map_sub₂ smulCommClass_left smulCommClass_self
tmul_neg 📖	mathematical	—	tmul AddCommGroup.toAddCommMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid TensorProduct neg	—	LinearMap.map_neg smulCommClass_left smulCommClass_self
tmul_sub 📖	mathematical	—	tmul AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup TensorProduct addCommGroup	—	LinearMap.map_sub smulCommClass_left smulCommClass_self
uncurry_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring TensorProduct addCommMonoid instModule LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero uncurry tmul	—	smulCommClass_self LinearMap.instSMulCommClass

TensorProduct.CompatibleSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
int 📖	mathematical	—	TensorProduct.CompatibleSMul Int.instMonoid AddCommGroup.toAddCommMonoid Module.toDistribMulAction Int.instSemiring AddCommGroup.toIntModule	—	Int.induction_on zero_smul TensorProduct.zero_tmul TensorProduct.tmul_zero AddMonoid.nat_smulCommClass' add_smul natCast_zsmul one_smul TensorProduct.add_tmul TensorProduct.tmul_add TensorProduct.tmul_smul isScalarTower AddCommMonoid.nat_isScalarTower AddRightCancelSemigroup.toIsRightCancelAdd sub_smul neg_smul TensorProduct.sub_tmul TensorProduct.tmul_sub
unit 📖	mathematical	—	TensorProduct.CompatibleSMul Units Units.instMonoid AddCommGroup.toAddCommMonoid Units.instDistribMulAction AddCommMonoid.toAddMonoid	—	smul_tmul

TensorProduct.Neg

Definitions

Name	Category	Theorems
aux 📖	CompOp	—

TensorProduct.lift

Definitions

Name	Category	Theorems
equiv 📖	CompOp	2 math math: equiv_symm_apply, equiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike LinearEquiv.instEquivLike equiv TensorProduct.tmul	—	smulCommClass_self TensorProduct.uncurry_apply
equiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm equiv TensorProduct.tmul	—	smulCommClass_self RingHomInvPair.ids LinearMap.instSMulCommClass
tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike TensorProduct.lift TensorProduct.tmul LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self
tmul' 📖	mathematical	—	DFunLike.coe AddHom TensorProduct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup TensorProduct.addCommMonoid AddHom.funLike LinearMap.toAddHom CommSemiring.toSemiring TensorProduct.instModule TensorProduct.lift TensorProduct.tmul LinearMap LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self
unique 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike TensorProduct.tmul LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	TensorProduct.lift	—	smulCommClass_self TensorProduct.ext' tmul

TensorProduct.liftAux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	mathematical	—	DFunLike.coe AddMonoidHom TensorProduct AddZeroClass.toAddZero TensorProduct.addZeroClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike TensorProduct.liftAux RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring TensorProduct.instSMul SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smulCommClass_self smulₛₗ
smulₛₗ 📖	mathematical	—	DFunLike.coe AddMonoidHom TensorProduct AddZeroClass.toAddZero TensorProduct.addZeroClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike TensorProduct.liftAux TensorProduct.instSMul SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	smulCommClass_self TensorProduct.induction_on smul_zero TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left LinearMap.map_smulₛₗ smul_add AddMonoidHom.map_add

---

← Back to Index