TensorProduct

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

Statistics

Metric	Count
Definitions maxTensorProduct, minTensorProduct	2
Theorems maxTensorProduct_comm, maxTensorProduct_map_le, maxTensorProduct_mono, mem_maxTensorProduct, minTensorProduct_comm, minTensorProduct_le_maxTensorProduct, minTensorProduct_map_le, minTensorProduct_mono, tmul_mem_maxTensorProduct, tmul_mem_minTensorProduct, tmul_subset_maxTensorProduct, tmul_subset_minTensorProduct	12
Total	14

PointedCone

Definitions

Name	Category	Theorems
maxTensorProduct 📖	CompOp	9 math math: maxTensorProduct_mono, minTensorProduct_eq_max_of_simplicial_generating_right, tmul_mem_maxTensorProduct, maxTensorProduct_map_le, tmul_subset_maxTensorProduct, minTensorProduct_le_maxTensorProduct, maxTensorProduct_comm, minTensorProduct_eq_max_of_simplicial_generating_left, mem_maxTensorProduct
minTensorProduct 📖	CompOp	8 math math: minTensorProduct_eq_max_of_simplicial_generating_right, minTensorProduct_mono, minTensorProduct_le_maxTensorProduct, tmul_subset_minTensorProduct, minTensorProduct_comm, minTensorProduct_map_le, minTensorProduct_eq_max_of_simplicial_generating_left, 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
maxTensorProduct_map_le 📖	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 map TensorProduct.map RingHom.id maxTensorProduct	—	IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono smulCommClass_self Algebra.to_smulCommClass RingHomCompTriple.ids TensorProduct.ext' DFunLike.congr_fun
maxTensorProduct_mono 📖	mathematical	PointedCone CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	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 maxTensorProduct	—	IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono smulCommClass_self Algebra.to_smulCommClass mem_maxTensorProduct dual_le_dual
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_hull
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
minTensorProduct_map_le 📖	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 map TensorProduct.map RingHom.id minTensorProduct	—	IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Submodule.map_span_le tmul_mem_minTensorProduct TensorProduct.map_tmul
minTensorProduct_mono 📖	mathematical	PointedCone CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	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	—	IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Submodule.span_mono Set.image2_subset
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 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 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 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 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