TensorProduct

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

Statistics

Metric	Count
Definitions maxTensorProduct, minTensorProduct	2
Theorems maxTensorProduct_comm, mem_maxTensorProduct, minTensorProduct_comm, minTensorProduct_le_maxTensorProduct, tmul_mem_maxTensorProduct, tmul_mem_minTensorProduct, tmul_subset_maxTensorProduct, tmul_subset_minTensorProduct	8
Total	10

PointedCone

Definitions

Name	Category	Theorems
maxTensorProduct 📖	CompOp	5 math math: tmul_mem_maxTensorProduct, tmul_subset_maxTensorProduct, minTensorProduct_le_maxTensorProduct, maxTensorProduct_comm, mem_maxTensorProduct
minTensorProduct 📖	CompOp	4 math math: minTensorProduct_le_maxTensorProduct, tmul_subset_minTensorProduct, minTensorProduct_comm, tmul_mem_minTensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
maxTensorProduct_comm 📖	mathematical	—	map TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid CommSemiring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing TensorProduct.addCommMonoid TensorProduct.instModule LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct.comm maxTensorProduct	—	IsStrictOrderedRing.toIsOrderedRing ext RingHomInvPair.ids IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono smulCommClass_self Algebra.to_smulCommClass TensorProduct.dualDistrib_apply_comm LinearEquiv.symm_apply_apply
mem_maxTensorProduct 📖	mathematical	—	TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PointedCone CommSemiring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing TensorProduct.addCommMonoid TensorProduct.instModule SetLike.instMembership Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule maxTensorProduct NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe Module.Dual LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.dualDistrib TensorProduct.tmul	—	IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono smulCommClass_self Algebra.to_smulCommClass dual_span
minTensorProduct_comm 📖	mathematical	—	map TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid CommSemiring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing TensorProduct.addCommMonoid TensorProduct.instModule LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct.comm minTensorProduct	—	IsStrictOrderedRing.toIsOrderedRing RingHomInvPair.ids IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Submodule.map_span Set.image_congr Set.image_image2 Set.image2_congr Set.image2_swap
minTensorProduct_le_maxTensorProduct 📖	mathematical	—	PointedCone TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid CommSemiring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing TensorProduct.addCommMonoid TensorProduct.instModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule minTensorProduct maxTensorProduct	—	IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Submodule.span_le tmul_subset_maxTensorProduct
tmul_mem_maxTensorProduct 📖	mathematical	PointedCone CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule maxTensorProduct TensorProduct.tmul	—	IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono smulCommClass_self mul_nonneg
tmul_mem_minTensorProduct 📖	mathematical	PointedCone CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule minTensorProduct TensorProduct.tmul	—	IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Submodule.subset_span Set.mem_image2_of_mem
tmul_subset_maxTensorProduct 📖	mathematical	—	Set TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set.instHasSubset Set.image2 TensorProduct.tmul SetLike.coe PointedCone CommSemiring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule TensorProduct.addCommMonoid TensorProduct.instModule maxTensorProduct	—	IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono tmul_mem_maxTensorProduct
tmul_subset_minTensorProduct 📖	mathematical	—	Set TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set.instHasSubset Set.image2 TensorProduct.tmul SetLike.coe PointedCone CommSemiring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule TensorProduct.addCommMonoid TensorProduct.instModule minTensorProduct	—	IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono tmul_mem_minTensorProduct

---

← Back to Index