TensorProduct

Statistics

Metric	Count
Definitions	0
Theorems `exists_rTensor_fg_inclusion_eq`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_rTensor_fg_inclusion_eq` 📖	mathematical	`Submodule.FG` `CommSemiring.toSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `Submodule.subtype`	`Submodule` `CommSemiring.toSemiring` `Submodule.FG` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `Submodule.inclusion`	—	`CanLift.prf` `Subtype.canLift` `Module.DirectLimit.exists_eq_of_of_eq` `TensorProduct.instDirectedSystemCoeLinearMapIdRTensor` `Module.fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId` `Module.fgSystem.instIsDirectedOrderSubtypeSubmoduleFG` `RingHomInvPair.ids` `TensorProduct.directLimitLeft_rTensor_of` `RingHomCompTriple.ids` `LinearEquiv.eq_toLinearMap_symm_comp` `Module.fgSystem.equiv_comp_of`

---