Documentation Verification Report

Module

📁 Source: Mathlib/Algebra/Order/Nonneg/Module.lean

Statistics

Metric	Count
Definitions `instModule`, `instSMul`, `instSMulWithZero`	3
Theorems `coe_smul`, `instIsOrderedModule`, `instIsScalarTower`, `instIsStrictOrderedModule`, `mk_smul`	5
Total	8

Nonneg

Definitions

Name	Category	Theorems
`instModule` 📖	CompOp	100 math math: `ProperCone.dual_insert`, `PointedCone.ofSubmodule_lineal`, `ProperCone.dual_sUnion`, `PointedCone.ofSubmodule_sSup`, `PointedCone.coe_ofSubmodule`, `ProperCone.innerDual_univ`, `ProperCone.coe_positive`, `PointedCone.dual_sup`, `PointedCone.DualFG.dual_dual_flip`, `PointedCone.dual_hull`, `ProperCone.mem_map`, `PointedCone.maxTensorProduct_mono`, `PointedCone.coe_map`, `PointedCone.subset_dual_dual`, `PointedCone.subset_hull`, `ProperCone.coe_bot`, `PointedCone.dual_ker`, `PointedCone.DualFG.exists_fg_dual`, `ProperCone.innerDual_sUnion`, `PointedCone.dual_union`, `PointedCone.tmul_mem_maxTensorProduct`, `PointedCone.DualFG.top`, `ProperCone.innerDual_zero`, `PointedCone.minTensorProduct_mono`, `PointedCone.ofSubmodule_sInf`, `PointedCone.mem_dual`, `PointedCone.DualFG.dual_flip_dual`, `PointedCone.dual_empty`, `PointedCone.lineal_eq_sSup`, `instModuleFinite`, `PointedCone.FG.dual_dualfg`, `PointedCone.maxTensorProduct_map_le`, `ProperCone.dual_univ`, `PointedCone.dual_insert`, `PointedCone.dual_antitone`, `PointedCone.basis_coord_mem_dual`, `ConvexCone.toPointedCone_top`, `PointedCone.convex`, `ProperCone.dual_iUnion`, `PointedCone.coe_lineal`, `PointedCone.mem_map`, `PointedCone.coe_closure`, `ProperCone.innerDual_union`, `PointedCone.tmul_subset_maxTensorProduct`, `ProperCone.dual_zero`, `PointedCone.dual_zero`, `PointedCone.minTensorProduct_le_maxTensorProduct`, `PointedCone.gc_ofSubmodule_lineal`, `PointedCone.tmul_subset_minTensorProduct`, `PointedCone.subset_span`, `PointedCone.ext_iff`, `ProperCone.innerDual_insert`, `PointedCone.dual_iUnion`, `PointedCone.coe_ofConeComb`, `PointedCone.mem_span_set`, `ProperCone.toPointedCone_bot`, `ProperCone.innerDual_empty`, `PointedCone.ofSubmodule_iSup`, `PointedCone.minTensorProduct_map_le`, `PointedCone.ofSubmodule_inf`, `PointedCone.dual_le_dual`, `PointedCone.mem_closure`, `PointedCone.subset_dual_flip_iff_subset_dual`, `ProperCone.mem_bot`, `ProperCone.dual_empty`, `PointedCone.DualFG.inf`, `PointedCone.support_eq`, `ProperCone.dual_union`, `PointedCone.mem_comap`, `PointedCone.tmul_mem_minTensorProduct`, `PointedCone.DualFG.dual_of_fg`, `PointedCone.mem_toConvexCone`, `PointedCone.isClosed_dual`, `PointedCone.mem_ofSubmodule_iff`, `PointedCone.mem_positive`, `ProperCone.innerDual_iUnion`, `PointedCone.mem_maxTensorProduct`, `PointedCone.dual_singleton_zero`, `PointedCone.dual_neg`, `PointedCone.dual_flip_dual_dual_flip`, `ProperCone.mem_toPointedCone`, `PointedCone.dual_sUnion`, `ProperCone.innerDual_toSubmodule`, `PointedCone.mem_hull_set`, `PointedCone.ofSubmodule_sup`, `PointedCone.ofSubmodule_iInf`, `ConvexCone.mem_toPointedCone`, `PointedCone.lineal_le`, `PointedCone.closure_eq`, `PointedCone.dual_anti`, `PointedCone.smul_mem`, `PointedCone.DualFG.iff_exists_fg_dual`, `PointedCone.dual_univ`, `PointedCone.dual_eq_iInter_dual_singleton`, `PointedCone.dual_dual_flip_dual`, `PointedCone.coe_comap`, `PointedCone.dual_eq_dual_id_map`, `PointedCone.mem_lineal`, `PointedCone.salient_iff_inter_neg_eq_singleton`, `PointedCone.dual_span`
`instSMul` 📖	CompOp	7 math math: `instIsScalarTower`, `mk_smul`, `instIsOrderedModule`, `instContinuousSMulSubtypeLeOfNat`, `coe_smul`, `instContinuousConstSMulSubtypeLeOfNat`, `instIsStrictOrderedModule`
`instSMulWithZero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSMul`	—	—
`instIsOrderedModule` 📖	mathematical	—	`IsOrderedModule` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulWithZero.toSMulZeroClass` `Subtype.preorder` `zero`	—	`PosSMulMono.smul_le_smul_of_nonneg_left` `IsOrderedModule.toPosSMulMono` `SMulPosMono.smul_le_smul_of_nonneg_right` `IsOrderedModule.toSMulPosMono`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSMul`	—	`SMul.comp.isScalarTower` `IsOrderedRing.toZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toPosMulMono`
`instIsStrictOrderedModule` 📖	mathematical	—	`IsStrictOrderedModule` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulWithZero.toSMulZeroClass` `Subtype.preorder` `zero`	—	`PosSMulStrictMono.smul_lt_smul_of_pos_left` `IsStrictOrderedModule.toPosSMulStrictMono` `SMulPosStrictMono.smul_lt_smul_of_pos_right` `IsStrictOrderedModule.toSMulPosStrictMono`
`mk_smul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSMul`	—	—

---

← Back to Index