TensorProduct

📁 Source: Mathlib/Algebra/Lie/TensorProduct.lean

Statistics

Metric	Count
Definitions toModuleHom, hasBracketAux, lieRingModule, liftLie, map, mapIncl	6
Theorems toModuleHom_apply, lieIdeal_oper_eq_tensor_map_range, coe_liftLie_eq_lift_coe, lieModule, lie_tmul_right, liftLie_apply, lift_apply, mapIncl_def, map_tmul, toLinearMap_map	10
Total	16

LieModule

Definitions

Name	Category	Theorems
toModuleHom 📖	CompOp	2 math math: toModuleHom_apply, LieSubmodule.lieIdeal_oper_eq_tensor_map_range

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toModuleHom_apply 📖	mathematical	—	DFunLike.coe LieModuleHom TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule TensorProduct.addCommGroup TensorProduct.instModule TensorProduct.LieModule.lieRingModule lieRingSelfModule lieAlgebraSelfModule LieModuleHom.instFunLike toModuleHom TensorProduct.tmul Bracket.bracket LieRingModule.toBracket	—	lieAlgebraSelfModule RingHomInvPair.ids smulCommClass_self LinearMap.instLieModule TensorProduct.LieModule.liftLie_apply

LieSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lieIdeal_oper_eq_tensor_map_range 📖	mathematical	—	Bracket.bracket LieIdeal LieSubmodule hasBracket LieModuleHom.range TensorProduct CommRing.toCommSemiring LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership instSetLike AddCommGroup.toAddCommMonoid AddSubgroupClass.toAddCommGroup instAddSubgroupClass SubmoduleClass.module CommSemiring.toSemiring AddCommGroup.toAddGroup instSMulMemClass TensorProduct.addCommGroup TensorProduct.instModule TensorProduct.LieModule.lieRingModule instLieRingModuleSubtypeMem instLieModule lieAlgebraSelfModule LieModuleHom.comp LieModule.toModuleHom TensorProduct.LieModule.mapIncl	—	instAddSubgroupClass instSMulMemClass instLieModule lieAlgebraSelfModule lieIdeal_oper_eq_linear_span RingHomSurjective.ids LieModuleHom.toSubmodule_range RingHomCompTriple.ids LieModuleHom.toLinearMap_comp LinearMap.range_comp TensorProduct.LieModule.mapIncl_def TensorProduct.LieModule.toLinearMap_map TensorProduct.range_map_eq_span_tmul Submodule.map_span LieModule.toModuleHom_apply

TensorProduct.LieModule

Definitions

Name	Category	Theorems
hasBracketAux 📖	CompOp	—
lieRingModule 📖	CompOp	12 math math: liftLie_apply, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieModule.weight_vector_multiplication, map_tmul, coe_liftLie_eq_lift_coe, LieModule.toModuleHom_apply, lift_apply, lie_tmul_right, toLinearMap_map, LieSubmodule.lieIdeal_oper_eq_tensor_map_range, lieModule, LieAlgebra.rootSpaceProduct_tmul
liftLie 📖	CompOp	2 math math: liftLie_apply, coe_liftLie_eq_lift_coe
map 📖	CompOp	3 math math: mapIncl_def, map_tmul, toLinearMap_map
mapIncl 📖	CompOp	2 math math: mapIncl_def, LieSubmodule.lieIdeal_oper_eq_tensor_map_range

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_liftLie_eq_lift_coe 📖	mathematical	—	DFunLike.coe LieModuleHom TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule lieRingModule LieModuleHom.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap LinearMap.addCommGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instLieRingModule LieModuleHom.instAddCommGroup LieModuleHom.instModule LinearMap.instLieModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv liftLie TensorProduct.addCommMonoid LinearMap.instFunLike LieModuleEquiv LinearMap.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero lieModule LieModuleEquiv.instEquivLike lift LieModuleHom.toLinearMap	—	smulCommClass_self RingHomInvPair.ids LinearMap.instLieModule
lieModule 📖	mathematical	—	LieModule TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule lieRingModule	—	TensorProduct.smulCommClass_left smulCommClass_self map_smul SemilinearMapClass.toMulActionSemiHomClass LieHom.instLinearMapClass LinearMap.rTensor_smul LinearMap.lTensor_smul smul_add LinearMap.semilinearMapClass
lie_tmul_right 📖	mathematical	—	Bracket.bracket TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRingModule.toBracket TensorProduct.addCommGroup lieRingModule TensorProduct.tmul TensorProduct.add	—	—
liftLie_apply 📖	mathematical	—	DFunLike.coe LieModuleHom TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule lieRingModule LieModuleHom.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap LinearMap.addCommGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instLieRingModule LieModuleHom.instAddCommGroup LieModuleHom.instModule LinearMap.instLieModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv liftLie TensorProduct.tmul LinearMap.instFunLike	—	smulCommClass_self RingHomInvPair.ids LinearMap.instLieModule LinearMap.instSMulCommClass lieModule coe_liftLie_eq_lift_coe
lift_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct AddCommGroup.toAddCommMonoid TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LieModuleEquiv LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.addCommGroup LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instLieRingModule LinearMap.instLieModule TensorProduct.addCommGroup lieRingModule lieModule EquivLike.toFunLike LieModuleEquiv.instEquivLike lift TensorProduct.tmul	—	smulCommClass_self LinearMap.instSMulCommClass LinearMap.instLieModule lieModule
mapIncl_def 📖	mathematical	—	mapIncl map LieSubmodule SetLike.instMembership LieSubmodule.instSetLike AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LieSubmodule.instLieRingModuleSubtypeMem LieSubmodule.instLieModule LieSubmodule.incl	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass LieSubmodule.instLieModule
map_tmul 📖	mathematical	—	DFunLike.coe LieModuleHom TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule lieRingModule LieModuleHom.instFunLike map TensorProduct.tmul	—	TensorProduct.map_tmul
toLinearMap_map 📖	mathematical	—	LieModuleHom.toLinearMap TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule lieRingModule map TensorProduct.map RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	—

---

← Back to Index