TensorProduct

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

Statistics

Metric	Count
Definitions	0
Theorems exists_rTensor_fg_inclusion_eq	1
Total	1

Submodule.FG

Theorems

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.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

---

← Back to Index