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	57 math math: `ProperCone.dual_insert`, `ProperCone.dual_sUnion`, `ProperCone.innerDual_univ`, `ProperCone.coe_positive`, `ProperCone.mem_map`, `PointedCone.coe_map`, `PointedCone.subset_dual_dual`, `ProperCone.coe_bot`, `ProperCone.innerDual_sUnion`, `PointedCone.dual_union`, `ProperCone.innerDual_zero`, `PointedCone.mem_dual`, `PointedCone.dual_empty`, `instModuleFinite`, `ProperCone.dual_univ`, `PointedCone.dual_insert`, `ConvexCone.toPointedCone_top`, `PointedCone.convex`, `ProperCone.dual_iUnion`, `PointedCone.mem_map`, `PointedCone.coe_closure`, `ProperCone.innerDual_union`, `PointedCone.tmul_subset_maxTensorProduct`, `ProperCone.dual_zero`, `PointedCone.dual_zero`, `PointedCone.minTensorProduct_le_maxTensorProduct`, `PointedCone.tmul_subset_minTensorProduct`, `PointedCone.subset_span`, `PointedCone.ext_iff`, `ProperCone.innerDual_insert`, `PointedCone.dual_iUnion`, `PointedCone.mem_span_set`, `ProperCone.toPointedCone_bot`, `ProperCone.innerDual_empty`, `PointedCone.dual_le_dual`, `PointedCone.mem_closure`, `ProperCone.mem_bot`, `ProperCone.dual_empty`, `ProperCone.dual_union`, `PointedCone.mem_comap`, `PointedCone.mem_toConvexCone`, `PointedCone.isClosed_dual`, `PointedCone.mem_positive`, `ProperCone.innerDual_iUnion`, `PointedCone.mem_maxTensorProduct`, `PointedCone.dual_flip_dual_dual_flip`, `ProperCone.mem_toPointedCone`, `PointedCone.dual_sUnion`, `ProperCone.innerDual_toSubmodule`, `ConvexCone.mem_toPointedCone`, `PointedCone.closure_eq`, `PointedCone.dual_univ`, `PointedCone.dual_eq_iInter_dual_singleton`, `PointedCone.dual_dual_flip_dual`, `PointedCone.coe_comap`, `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`	`instSMul`	—	—

---

← Back to Index