TensorProduct

📁 Source: Mathlib/Analysis/Convex/Cone/TensorProduct.lean

Statistics

Metric	Count
Definitions	0
Theorems basis_coord_mem_dual, minTensorProduct_eq_max_of_simplicial_generating_left, minTensorProduct_eq_max_of_simplicial_generating_right	3
Total	3

PointedCone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_coord_mem_dual 📖	mathematical	Set Set.instHasSubset SetLike.coe PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule hull Set.range DFunLike.coe Module.Basis Module.Basis.instFunLike	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule PointedCone Module.Dual LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.instMembership Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule dual LinearMap.flip Module.dualPairing SetLike.coe Module.Basis.coord	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono dual_le_dual smulCommClass_self Algebra.to_smulCommClass dual_hull RingHomInvPair.ids Module.Basis.repr_self Finsupp.single_apply ite_nonneg zero_le_one le_rfl
minTensorProduct_eq_max_of_simplicial_generating_left 📖	mathematical	IsSimplicial Real Real.semiring Real.partialOrder Real.instIsOrderedRing AddCommGroup.toAddCommMonoid Submodule.span SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule Top.top Submodule Submodule.instTop	minTensorProduct Real Real.commRing Real.linearOrder Real.instIsStrictOrderedRing ProperCone.toPointedCone Real.semiring Real.partialOrder Real.instIsOrderedRing AddCommGroup.toAddCommMonoid maxTensorProduct	—	Real.instIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing mem_hull_set SetLike.mem_coe Submodule.sum_mem Submodule.smul_mem Submodule.subset_span Subtype.range_coe Submodule.span_le smulCommClass_self basis_coord_mem_dual Submodule.span_mono Subtype.range_coe_subtype Set.instReflSubset le_antisymm minTensorProduct_le_maxTensorProduct RingHomInvPair.ids LinearEquiv.symm_apply_apply TensorProduct.equivFinsuppOfBasisLeft_symm_apply Finsupp.sum_fintype TensorProduct.tmul_zero tmul_mem_minTensorProduct subset_hull Subtype.prop TensorProduct.equivFinsuppOfBasisLeft_apply instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid instIsTopologicalAddGroupReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsSemitopologicalSemiring.toContinuousAdd topDualPairing_isContPerfPair Real.instCompleteSpace LinearMap.flip.instIsContPerfPair ProperCone.dual_dual_flip RingHomCompTriple.ids TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.left IsScalarTower.right LinearMap.ext IsScalarTower.to_smulCommClass mul_comm map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
minTensorProduct_eq_max_of_simplicial_generating_right 📖	mathematical	IsSimplicial Real Real.semiring Real.partialOrder Real.instIsOrderedRing AddCommGroup.toAddCommMonoid Submodule.span SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule Top.top Submodule Submodule.instTop	minTensorProduct Real Real.commRing Real.linearOrder Real.instIsStrictOrderedRing ProperCone.toPointedCone Real.semiring Real.partialOrder Real.instIsOrderedRing AddCommGroup.toAddCommMonoid maxTensorProduct	—	Real.instIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing RingHomInvPair.ids minTensorProduct_comm maxTensorProduct_comm minTensorProduct_eq_max_of_simplicial_generating_left

---

← Back to Index