Defs

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

Statistics

Metric	Count
Definitions `IsOrderedModule`, `IsStrictOrderedModule`, `smulRight`, `PosSMulMono`, `PosSMulReflectLE`, `PosSMulReflectLT`, `PosSMulStrictMono`, `SMulPosMono`, `SMulPosReflectLE`, `SMulPosReflectLT`, `SMulPosStrictMono`	11
Theorems `of_smul_nonneg`, `toPosSMulMono`, `toSMulPosMono`, `toIsOrderedModule`, `toIsOrderedModule`, `toPosSMulStrictMono`, `toSMulPosStrictMono`, `toIsStrictOrderedModule`, `toSMulPosMono`, `toSMulPosReflectLE`, `toSMulPosReflectLT`, `toSMulPosStrictMono`, `instIsOrderedModule`, `instIsStrictOrderedModule`, `instPosSMulMono`, `instPosSMulReflectLE`, `instPosSMulReflectLT`, `instPosSMulStrictMono`, `instSMulPosMono`, `instSMulPosReflectLE`, `instSMulPosReflectLT`, `instSMulPosStrictMono`, `smulRight_apply`, `smulRight_symm_apply`, `toPosSMulMonoNat`, `toSMulPosMonoNat`, `instPosSMulMono`, `instPosSMulReflectLE`, `instPosSMulStrictMono`, `instSMulPosMono`, `instSMulPosReflectLE`, `instSMulPosReflectLT`, `instSMulPosStrictMono`, `toPosSMulMono`, `toPosSMulReflectLE`, `toPosSMulReflectLT`, `toPosSMulStrictMono`, `of_pos`, `of_smul_nonneg`, `smul_le_smul_of_nonneg_left`, `toPosSMulReflectLT`, `toPosSMulStrictMono`, `toSMulPosMono`, `le_of_smul_le_smul_left`, `toPosSMulReflectLT`, `toPosSMulStrictMono`, `PosSMulReflectLE_iff_posSMulReflectLT`, `lt_of_smul_lt_smul_left`, `of_pos`, `toPosSMulMono`, `toPosSMulReflectLE`, `smul_lt_smul_of_pos_left`, `toPosSMulMono`, `toPosSMulReflectLE`, `toSMulPosStrictMono`, `instPosSMulMono`, `instPosSMulReflectLE`, `instPosSMulStrictMono`, `instSMulPosMono`, `instSMulPosReflectLE`, `instSMulPosReflectLT`, `instSMulPosStrictMono`, `of_pos`, `smul_le_smul_of_nonneg_right`, `toSMulPosReflectLT`, `toSMulPosStrictMono`, `le_of_smul_le_smul_right`, `toSMulPosReflectLT`, `toSMulPosStrictMono`, `SMulPosReflectLE_iff_smulPosReflectLT`, `lt_of_smul_lt_smul_right`, `of_pos`, `toSMulPosMono`, `toSMulPosReflectLE`, `smul_lt_smul_of_pos_right`, `toSMulPosMono`, `toSMulPosReflectLE`, `toPosSMulStrictMonoNat`, `toSMulPosStrictMonoNat`, `antitone_smul_left`, `instPosSMulMonoNatOfIsOrderedAddMonoid`, `instPosSMulStrictMonoIntOfIsOrderedAddMonoid`, `instPosSMulStrictMonoNatOfIsOrderedAddMonoid`, `instSMulPosMonoNatOfIsOrderedAddMonoid`, `instSMulPosStrictMonoIntOfIsOrderedAddMonoid`, `instSMulPosStrictMonoNatOfIsOrderedCancelAddMonoid`, `inv_smul_le_iff_of_pos`, `inv_smul_lt_iff_of_pos`, `le_inv_smul_iff_of_pos`, `le_of_smul_le_smul_left`, `le_of_smul_le_smul_of_neg`, `le_of_smul_le_smul_of_pos_left`, `le_of_smul_le_smul_of_pos_right`, `le_of_smul_le_smul_right`, `le_smul_iff_one_le_left`, `le_smul_of_one_le_left`, `lt_inv_smul_iff_of_pos`, `lt_of_smul_lt_smul_left`, `lt_of_smul_lt_smul_of_nonneg_left`, `lt_of_smul_lt_smul_of_nonneg_right`, `lt_of_smul_lt_smul_of_nonpos`, `lt_of_smul_lt_smul_right`, `lt_smul_iff_one_lt_left`, `lt_smul_of_one_lt_left`, `monotone_smul_left_of_nonneg`, `monotone_smul_right_of_nonneg`, `neg_iff_neg_of_smul_pos`, `neg_of_smul_neg_left`, `neg_of_smul_neg_left'`, `neg_of_smul_neg_right`, `neg_of_smul_neg_right'`, `neg_of_smul_pos_left`, `neg_of_smul_pos_right`, `nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg`, `posSMulMono_iff_posSMulReflectLT`, `posSMulMono_iff_posSMulStrictMono`, `posSMulStrictMono_iff_PosSMulReflectLE`, `pos_and_pos_or_neg_and_neg_of_smul_pos`, `pos_iff_pos_of_smul_pos`, `pos_of_smul_pos_left`, `pos_of_smul_pos_right`, `smulPosMono_iff_smulPosReflectLT`, `smulPosMono_iff_smulPosStrictMono`, `smulPosStrictMono_iff_SMulPosReflectLE`, `smul_add_smul_le_smul_add_smul`, `smul_add_smul_le_smul_add_smul'`, `smul_add_smul_lt_smul_add_smul`, `smul_add_smul_lt_smul_add_smul'`, `smul_eq_smul_iff_eq_and_eq_of_pos`, `smul_eq_smul_iff_eq_and_eq_of_pos'`, `smul_le_iff_le_one_left`, `smul_le_of_le_one_left`, `smul_le_smul`, `smul_le_smul'`, `smul_le_smul_iff_of_neg_left`, `smul_le_smul_iff_of_pos_left`, `smul_le_smul_iff_of_pos_right`, `smul_le_smul_of_nonneg_left`, `smul_le_smul_of_nonneg_right`, `smul_le_smul_of_nonpos_left`, `smul_lt_iff_lt_one_left`, `smul_lt_of_lt_one_left`, `smul_lt_smul`, `smul_lt_smul'`, `smul_lt_smul_iff_of_neg_left`, `smul_lt_smul_iff_of_pos_left`, `smul_lt_smul_iff_of_pos_right`, `smul_lt_smul_of_le_of_lt`, `smul_lt_smul_of_le_of_lt'`, `smul_lt_smul_of_lt_of_le`, `smul_lt_smul_of_lt_of_le'`, `smul_lt_smul_of_neg_left`, `smul_lt_smul_of_pos_left`, `smul_lt_smul_of_pos_right`, `smul_max_of_nonneg`, `smul_max_of_nonpos`, `smul_min_of_nonneg`, `smul_min_of_nonpos`, `smul_neg_iff_of_neg_left`, `smul_neg_iff_of_pos_left`, `smul_neg_of_neg_of_pos`, `smul_neg_of_pos_of_neg`, `smul_nonneg`, `smul_nonneg'`, `smul_nonneg_iff`, `smul_nonneg_iff_neg_imp_nonpos`, `smul_nonneg_iff_pos_imp_nonneg`, `smul_nonneg_of_nonpos_of_nonpos`, `smul_nonpos_iff`, `smul_nonpos_iff_neg_imp_nonneg`, `smul_nonpos_iff_pos_imp_nonpos`, `smul_nonpos_of_nonneg_of_nonpos`, `smul_nonpos_of_nonpos_of_nonneg`, `smul_pos`, `smul_pos'`, `smul_pos_iff_of_neg_left`, `smul_pos_iff_of_pos_left`, `smul_pos_iff_of_pos_right`, `smul_pos_of_neg_of_neg`, `strictAnti_smul_left`, `strictMono_smul_left_of_pos`, `strictMono_smul_right_of_pos`	182
Total	193

IsOrderedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_smul_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`IsOrderedModule` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`PosSMulMono.of_smul_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_smul`
`toPosSMulMono` 📖	mathematical	—	`PosSMulMono`	—	—
`toSMulPosMono` 📖	mathematical	—	`SMulPosMono`	—	—

IsOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsOrderedModule` 📖	mathematical	—	`IsOrderedModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`PosMulMono.toPosSMulMono` `toPosMulMono` `MulPosMono.toSMulPosMono` `toMulPosMono`

IsStrictOrderedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsOrderedModule` 📖	mathematical	—	`IsOrderedModule` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder`	—	`PosSMulStrictMono.toPosSMulMono` `toPosSMulStrictMono` `SMulPosStrictMono.toSMulPosMono` `toSMulPosStrictMono`
`toPosSMulStrictMono` 📖	mathematical	—	`PosSMulStrictMono`	—	—
`toSMulPosStrictMono` 📖	mathematical	—	`SMulPosStrictMono`	—	—

IsStrictOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsStrictOrderedModule` 📖	mathematical	—	`IsStrictOrderedModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`PosMulStrictMono.toPosSMulStrictMono` `toPosMulStrictMono` `MulPosStrictMono.toSMulPosStrictMono` `toMulPosStrictMono`

MulPosMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toSMulPosMono` 📖	mathematical	—	`SMulPosMono`	—	`mul_le_mul_of_nonneg_right`

MulPosReflectLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toSMulPosReflectLE` 📖	mathematical	—	`SMulPosReflectLE`	—	`le_of_mul_le_mul_right`

MulPosReflectLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toSMulPosReflectLT` 📖	mathematical	—	`SMulPosReflectLT`	—	`lt_of_mul_lt_mul_right`

MulPosStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toSMulPosStrictMono` 📖	mathematical	—	`SMulPosStrictMono`	—	`mul_lt_mul_of_pos_right`

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsOrderedModule` 📖	mathematical	—	`IsOrderedModule` `OrderDual` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `instPreorder` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `instZeroOrderDual` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`instPosSMulMono` `IsOrderedModule.toPosSMulMono` `instSMulPosMono` `IsOrderedModule.toSMulPosMono`
`instIsStrictOrderedModule` 📖	mathematical	—	`IsStrictOrderedModule` `OrderDual` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `instPreorder` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `instZeroOrderDual` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`instPosSMulStrictMono` `IsStrictOrderedModule.toPosSMulStrictMono` `instSMulPosStrictMono` `IsStrictOrderedModule.toSMulPosStrictMono`
`instPosSMulMono` 📖	mathematical	—	`PosSMulMono` `OrderDual` `instSMul` `instPreorder`	—	`smul_le_smul_of_nonneg_left`
`instPosSMulReflectLE` 📖	mathematical	—	`PosSMulReflectLE` `OrderDual` `instSMul` `instPreorder`	—	`le_of_smul_le_smul_of_pos_left`
`instPosSMulReflectLT` 📖	mathematical	—	`PosSMulReflectLT` `OrderDual` `instSMul` `instPreorder`	—	`lt_of_smul_lt_smul_of_nonneg_left`
`instPosSMulStrictMono` 📖	mathematical	—	`PosSMulStrictMono` `OrderDual` `instSMul` `instPreorder`	—	`smul_lt_smul_of_pos_left`
`instSMulPosMono` 📖	mathematical	—	`SMulPosMono` `OrderDual` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instPreorder` `PartialOrder.toPreorder` `instZeroOrderDual` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`neg_le_neg_iff` `addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `addRightMono` `covariant_swap_add_of_covariant_add` `AddMonoid.zero_add` `AddMonoid.add_zero` `smul_neg` `smul_le_smul_of_nonneg_right` `neg_nonneg`
`instSMulPosReflectLE` 📖	mathematical	—	`SMulPosReflectLE` `OrderDual` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instPreorder` `PartialOrder.toPreorder` `instZeroOrderDual` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`le_of_smul_le_smul_right` `AddMonoid.zero_add` `AddMonoid.add_zero` `smul_neg` `neg_le_neg_iff` `addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `addRightMono` `covariant_swap_add_of_covariant_add` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`instSMulPosReflectLT` 📖	mathematical	—	`SMulPosReflectLT` `OrderDual` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instPreorder` `PartialOrder.toPreorder` `instZeroOrderDual` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`lt_of_smul_lt_smul_right` `AddMonoid.zero_add` `AddMonoid.add_zero` `smul_neg` `neg_lt_neg_iff` `addLeftStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `addRightStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `neg_nonneg`
`instSMulPosStrictMono` 📖	mathematical	—	`SMulPosStrictMono` `OrderDual` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instPreorder` `PartialOrder.toPreorder` `instZeroOrderDual` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`neg_lt_neg_iff` `addLeftStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `addRightStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `AddMonoid.zero_add` `AddMonoid.add_zero` `smul_neg` `smul_lt_smul_of_pos_right` `neg_pos`

OrderIso

Definitions

Name	Category	Theorems
`smulRight` 📖	CompOp	2 math math: `smulRight_apply`, `smulRight_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smulRight_apply` 📖	mathematical	`Preorder.toLT` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`DFunLike.coe` `RelIso` `Preorder.toLE` `RelIso.instFunLike` `smulRight` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction`	—	—
`smulRight_symm_apply` 📖	mathematical	`Preorder.toLT` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`DFunLike.coe` `RelIso` `Preorder.toLE` `RelIso.instFunLike` `RelIso.symm` `smulRight` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	—

OrderedSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPosSMulMonoNat` 📖	mathematical	—	`PosSMulMono` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.instPreorder` `PartialOrder.toPreorder` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`nsmul_le_nsmul_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`toSMulPosMonoNat` 📖	mathematical	—	`SMulPosMono` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.instPreorder` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`nsmul_le_nsmul_left` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instPosSMulMono` 📖	mathematical	`PosSMulMono`	`instSMul` `preorder`	—	`smul_le_smul_of_nonneg_left`
`instPosSMulReflectLE` 📖	mathematical	`PosSMulReflectLE`	`instSMul` `preorder`	—	`le_of_smul_le_smul_left`
`instPosSMulStrictMono` 📖	mathematical	`PosSMulStrictMono` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder`	`instSMul` `preorder`	—	`smul_le_smul_of_nonneg_left` `instPosSMulMono` `PosSMulStrictMono.toPosSMulMono` `LT.lt.le` `smul_lt_smul_of_pos_left`
`instSMulPosMono` 📖	mathematical	`SMulPosMono`	`instSMul` `preorder` `instZero`	—	`smul_le_smul_of_nonneg_right`
`instSMulPosReflectLE` 📖	mathematical	`SMulPosReflectLE`	`instSMul` `preorder` `instZero`	—	`lt_def` `le_of_smul_le_smul_right`
`instSMulPosReflectLT` 📖	mathematical	`SMulPosReflectLT` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder`	`instSMul` `preorder` `instZero`	—	`lt_of_smul_lt_smul_right`
`instSMulPosStrictMono` 📖	mathematical	`SMulPosStrictMono` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder`	`instSMul` `preorder` `instZero`	—	`smul_le_smul_of_nonneg_right` `instSMulPosMono` `SMulPosStrictMono.toSMulPosMono` `LT.lt.le` `smul_lt_smul_of_pos_right`

PosMulMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPosSMulMono` 📖	mathematical	—	`PosSMulMono`	—	`mul_le_mul_of_nonneg_left`

PosMulReflectLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPosSMulReflectLE` 📖	mathematical	—	`PosSMulReflectLE`	—	`le_of_mul_le_mul_left`

PosMulReflectLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPosSMulReflectLT` 📖	mathematical	—	`PosSMulReflectLT`	—	`lt_of_mul_lt_mul_left`

PosMulStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPosSMulStrictMono` 📖	mathematical	—	`PosSMulStrictMono`	—	`mul_lt_mul_of_pos_left`

PosSMulMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_pos` 📖	mathematical	`Preorder.toLE` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	`PosSMulMono` `PartialOrder.toPreorder`	—	`LE.le.eq_or_lt` `zero_smul`
`of_smul_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`PosSMulMono` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `smul_sub`
`smul_le_smul_of_nonneg_left` 📖	—	`Preorder.toLE`	—	—	—
`toPosSMulReflectLT` 📖	mathematical	—	`PosSMulReflectLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Monotone.reflect_lt` `monotone_smul_left_of_nonneg`
`toPosSMulStrictMono` 📖	mathematical	—	`PosSMulStrictMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`LE.le.lt_of_ne` `smul_le_smul_of_nonneg_left` `LT.lt.le` `smul_right_injective` `IsDomain.toIsCancelMulZero` `LT.lt.ne'` `LT.lt.ne`
`toSMulPosMono` 📖	mathematical	—	`SMulPosMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_smul` `smul_nonneg` `IsOrderedRing.toIsOrderedAddMonoid`

PosSMulReflectLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_of_smul_le_smul_left` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	—
`toPosSMulReflectLT` 📖	mathematical	—	`PosSMulReflectLT` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder`	—	`PosSMulReflectLT.of_pos` `LE.le.lt_of_ne` `le_of_smul_le_smul_of_pos_left` `LT.lt.le`
`toPosSMulStrictMono` 📖	mathematical	—	`PosSMulStrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`not_le` `LT.lt.not_ge` `le_of_smul_le_smul_left`

PosSMulReflectLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_of_smul_lt_smul_left` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	—
`of_pos` 📖	mathematical	`Preorder.toLT`	`PosSMulReflectLT` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder`	—	`LE.le.eq_or_lt` `zero_smul`
`toPosSMulMono` 📖	mathematical	—	`PosSMulMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`not_lt` `LE.le.not_gt` `lt_of_smul_lt_smul_left`
`toPosSMulReflectLE` 📖	mathematical	—	`PosSMulReflectLE` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`LE.le.eq_or_lt` `Eq.le` `smul_right_injective` `IsDomain.toIsCancelMulZero` `LT.lt.ne'` `LT.lt.le` `lt_of_smul_lt_smul_left`

PosSMulStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_lt_smul_of_pos_left` 📖	—	`Preorder.toLT`	—	—	—
`toPosSMulMono` 📖	mathematical	—	`PosSMulMono` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder`	—	`PosSMulMono.of_pos` `StrictMono.monotone` `strictMono_smul_left_of_pos`
`toPosSMulReflectLE` 📖	mathematical	—	`PosSMulReflectLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`StrictMono.le_iff_le` `strictMono_smul_left_of_pos`
`toSMulPosStrictMono` 📖	mathematical	—	`SMulPosStrictMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_smul` `smul_pos` `IsOrderedRing.toIsOrderedAddMonoid`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instPosSMulMono` 📖	mathematical	—	`PosSMulMono` `instSMul` `instPreorder`	—	`smul_le_smul_of_nonneg_left`
`instPosSMulReflectLE` 📖	mathematical	—	`PosSMulReflectLE` `instSMul` `instPreorder`	—	`le_of_smul_le_smul_left`
`instPosSMulStrictMono` 📖	mathematical	—	`PosSMulStrictMono` `instSMul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder` `instPreorder`	—	`smul_lt_smul_of_pos_left` `smul_le_smul_of_nonneg_left` `PosSMulStrictMono.toPosSMulMono` `LT.lt.le`
`instSMulPosMono` 📖	mathematical	—	`SMulPosMono` `instSMul` `instPreorder` `instZero`	—	`smul_le_smul_of_nonneg_right`
`instSMulPosReflectLE` 📖	mathematical	—	`SMulPosReflectLE` `instSMul` `instPreorder` `instZero`	—	`lt_iff` `le_of_smul_le_smul_right`
`instSMulPosReflectLT` 📖	mathematical	—	`SMulPosReflectLT` `instSMul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder` `instPreorder` `instZero`	—	`lt_of_smul_lt_smul_right`
`instSMulPosStrictMono` 📖	mathematical	—	`SMulPosStrictMono` `instSMul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder` `instPreorder` `instZero`	—	`smul_lt_smul_of_pos_right` `smul_le_smul_of_nonneg_right` `SMulPosStrictMono.toSMulPosMono` `LT.lt.le`

SMulPosMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_pos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	`SMulPosMono`	—	`LE.le.eq_or_lt` `smul_zero`
`smul_le_smul_of_nonneg_right` 📖	—	`Preorder.toLE`	—	—	—
`toSMulPosReflectLT` 📖	mathematical	—	`SMulPosReflectLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`not_le` `LT.lt.not_ge` `smul_le_smul_of_nonneg_right`
`toSMulPosStrictMono` 📖	mathematical	—	`SMulPosStrictMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`LE.le.lt_of_ne` `smul_le_smul_of_nonneg_right` `LT.lt.le` `smul_left_injective` `IsDomain.toIsCancelMulZero` `LT.lt.ne'` `LT.lt.ne`

SMulPosReflectLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_of_smul_le_smul_right` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	—
`toSMulPosReflectLT` 📖	mathematical	—	`SMulPosReflectLT` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder`	—	`SMulPosReflectLT.of_pos` `LE.le.lt_of_ne` `le_of_smul_le_smul_of_pos_right` `LT.lt.le`
`toSMulPosStrictMono` 📖	mathematical	—	`SMulPosStrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`not_le` `LT.lt.not_ge` `le_of_smul_le_smul_of_pos_right`

SMulPosReflectLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_of_smul_lt_smul_right` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	—
`of_pos` 📖	mathematical	`Preorder.toLT`	`SMulPosReflectLT` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder`	—	`LE.le.eq_or_lt` `smul_zero`
`toSMulPosMono` 📖	mathematical	—	`SMulPosMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`not_lt` `LE.le.not_gt` `lt_of_smul_lt_smul_right`
`toSMulPosReflectLE` 📖	mathematical	—	`SMulPosReflectLE` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`LE.le.eq_or_lt` `Eq.le` `smul_left_injective` `IsDomain.toIsCancelMulZero` `LT.lt.ne'` `LT.lt.le` `lt_of_smul_lt_smul_right`

SMulPosStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_lt_smul_of_pos_right` 📖	—	`Preorder.toLT`	—	—	—
`toSMulPosMono` 📖	mathematical	—	`SMulPosMono` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `PartialOrder.toPreorder`	—	`SMulPosMono.of_pos` `StrictMono.monotone` `strictMono_smul_right_of_pos`
`toSMulPosReflectLE` 📖	mathematical	—	`SMulPosReflectLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`not_lt` `LE.le.not_gt` `smul_lt_smul_of_pos_right`

StrictOrderedSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPosSMulStrictMonoNat` 📖	mathematical	—	`PosSMulStrictMono` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.instPreorder` `PartialOrder.toPreorder` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`nsmul_right_strictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `LT.lt.ne'`
`toSMulPosStrictMonoNat` 📖	mathematical	—	`SMulPosStrictMono` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.instPreorder` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`nsmul_lt_nsmul_left` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`

(root)

Definitions

Name	Category	Theorems
`IsOrderedModule` 📖	CompData	7 math math: `IsStrictOrderedModule.toIsOrderedModule`, `instIsOrderedModule`, `IsOrderedModule.of_smul_nonneg`, `Nonneg.instIsOrderedModule`, `OrderDual.instIsOrderedModule`, `PointedCone.to_isOrderedModule`, `IsOrderedRing.toIsOrderedModule`
`IsStrictOrderedModule` 📖	CompData	8 math math: `OrderDual.instIsStrictOrderedModule`, `RCLike.toIsStrictOrderedModule`, `IsStrictOrderedRing.toIsStrictOrderedModule`, `DivisibleHull.instIsStrictOrderedModuleNNRat`, `instIsStrictOrderedModuleOfIsCancelAdd`, `DivisibleHull.instIsStrictOrderedModuleRat`, `NNReal.instIsStrictOrderedModule`, `Nonneg.instIsStrictOrderedModule`
`PosSMulMono` 📖	CompData	15 math math: `IsOrderedModule.toPosSMulMono`, `OrderDual.instPosSMulMono`, `PosSMulStrictMono.toPosSMulMono`, `PosSMulMono.lift`, `PosSMulMono.of_pos`, `PosSMulMono.nnrat_of_rat`, `OrderedSemiring.toPosSMulMonoNat`, `instPosSMulMonoNatOfIsOrderedAddMonoid`, `PosSMulReflectLT.toPosSMulMono`, `posSMulMono_iff_posSMulReflectLT`, `Finsupp.instPosSMulMono`, `PosMulMono.toPosSMulMono`, `Prod.instPosSMulMono`, `posSMulMono_iff_posSMulStrictMono`, `PosSMulMono.of_smul_nonneg`
`PosSMulReflectLE` 📖	CompData	10 math math: `Finsupp.instPosSMulReflectLE`, `PosSMulReflectLE_iff_posSMulReflectLT`, `OrderDual.instPosSMulReflectLE`, `Prod.instPosSMulReflectLE`, `posSMulStrictMono_iff_PosSMulReflectLE`, `PosMulReflectLE.toPosSMulReflectLE`, `PosSMulStrictMono.toPosSMulReflectLE`, `PosSMulReflectLT.toPosSMulReflectLE`, `PosSMulReflectLE.lift`, `PosSMulMono.toPosSMulReflectLE`
`PosSMulReflectLT` 📖	CompData	10 math math: `PosSMulReflectLE_iff_posSMulReflectLT`, `PosSMulReflectLT.of_pos`, `PosSMulReflectLT.lift`, `OrderDual.instPosSMulReflectLT`, `posSMulMono_iff_posSMulReflectLT`, `OrderedSMul.toPosSMulReflectLT`, `PosMulReflectLT.toPosSMulReflectLT`, `PosSMulReflectLE.toPosSMulReflectLT`, `PosSMulMono.toPosSMulReflectLT`, `PosSMulStrictMono.toPosSMulReflectLT`
`PosSMulStrictMono` 📖	CompData	20 math math: `instPosSMulStrictMonoIntOfIsOrderedAddMonoid`, `IsStrictOrderedModule.toPosSMulStrictMono`, `NNReal.instPosSMulStrictMono`, `posSMulStrictMono_iff_PosSMulReflectLE`, `instPosSMulStrictMono`, `OrderedSMul.toPosSMulStrictMono`, `Finsupp.instPosSMulStrictMono`, `PosSMulStrictMono.lift`, `OrderDual.instPosSMulStrictMono`, `PosMulStrictMono.toPosSMulStrictMono`, `PosSMulStrictMono.nnrat_of_rat`, `PosSMulMono.toPosSMulStrictMono`, `LinearOrderedSemifield.toPosSMulStrictMono_rat`, `posSMulMono_iff_posSMulStrictMono`, `StrictOrderedSemiring.toPosSMulStrictMonoNat`, `ENNReal.instPosSMulStrictMonoNNReal`, `Prod.instPosSMulStrictMono`, `instPosSMulStrictMonoNatOfIsOrderedAddMonoid`, `PosSMulReflectLE.toPosSMulStrictMono`, `LinearOrderedField.toPosSMulStrictMono_rat`
`SMulPosMono` 📖	CompData	15 math math: `MulPosMono.toSMulPosMono`, `smulPosMono_iff_smulPosStrictMono`, `SMulPosMono.lift`, `IsOrderedModule.toSMulPosMono`, `ENNReal.instSMulPosMonoNNReal`, `SMulPosStrictMono.toSMulPosMono`, `SMulPosMono.of_pos`, `Finsupp.instSMulPosMono`, `OrderDual.instSMulPosMono`, `PosSMulMono.toSMulPosMono`, `OrderedSemiring.toSMulPosMonoNat`, `SMulPosReflectLT.toSMulPosMono`, `instSMulPosMonoNatOfIsOrderedAddMonoid`, `smulPosMono_iff_smulPosReflectLT`, `Prod.instSMulPosMono`
`SMulPosReflectLE` 📖	CompData	9 math math: `Finsupp.instSMulPosReflectLE`, `SMulPosReflectLE_iff_smulPosReflectLT`, `smulPosStrictMono_iff_SMulPosReflectLE`, `OrderDual.instSMulPosReflectLE`, `SMulPosReflectLT.toSMulPosReflectLE`, `SMulPosReflectLE.lift`, `MulPosReflectLE.toSMulPosReflectLE`, `Prod.instSMulPosReflectLE`, `SMulPosStrictMono.toSMulPosReflectLE`
`SMulPosReflectLT` 📖	CompData	10 math math: `SMulPosReflectLE_iff_smulPosReflectLT`, `SMulPosMono.toSMulPosReflectLT`, `Finsupp.instSMulPosReflectLT`, `SMulPosReflectLT.lift`, `MulPosReflectLT.toSMulPosReflectLT`, `OrderDual.instSMulPosReflectLT`, `SMulPosReflectLE.toSMulPosReflectLT`, `SMulPosReflectLT.of_pos`, `Prod.instSMulPosReflectLT`, `smulPosMono_iff_smulPosReflectLT`
`SMulPosStrictMono` 📖	CompData	15 math math: `smulPosMono_iff_smulPosStrictMono`, `smulPosStrictMono_iff_SMulPosReflectLE`, `OrderDual.instSMulPosStrictMono`, `SMulPosStrictMono.lift`, `MulPosStrictMono.toSMulPosStrictMono`, `StrictOrderedSemiring.toSMulPosStrictMonoNat`, `Prod.instSMulPosStrictMono`, `Finsupp.instSMulPosStrictMono`, `instSMulPosStrictMonoIntOfIsOrderedAddMonoid`, `instSMulPosStrictMonoNatOfIsOrderedCancelAddMonoid`, `SMulPosMono.toSMulPosStrictMono`, `NNReal.instSMulPosStrictMono`, `SMulPosReflectLE.toSMulPosStrictMono`, `PosSMulStrictMono.toSMulPosStrictMono`, `IsStrictOrderedModule.toSMulPosStrictMono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`PosSMulReflectLE_iff_posSMulReflectLT` 📖	mathematical	—	`PosSMulReflectLE` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `PosSMulReflectLT`	—	`PosSMulReflectLE.toPosSMulReflectLT` `PosSMulReflectLT.toPosSMulReflectLE`
`SMulPosReflectLE_iff_smulPosReflectLT` 📖	mathematical	—	`SMulPosReflectLE` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulPosReflectLT`	—	`SMulPosReflectLE.toSMulPosReflectLT` `SMulPosReflectLT.toSMulPosReflectLE`
`antitone_smul_left` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Antitone` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_le_smul_of_nonpos_left`
`instPosSMulMonoNatOfIsOrderedAddMonoid` 📖	mathematical	—	`PosSMulMono` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `Nat.instPreorder` `PartialOrder.toPreorder` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`nsmul_le_nsmul_right` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`instPosSMulStrictMonoIntOfIsOrderedAddMonoid` 📖	mathematical	—	`PosSMulStrictMono` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	—	`zsmul_lt_zsmul_right`
`instPosSMulStrictMonoNatOfIsOrderedAddMonoid` 📖	mathematical	—	`PosSMulStrictMono` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Nat.instPreorder` `PartialOrder.toPreorder` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`nsmul_lt_nsmul_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `LT.lt.ne'`
`instSMulPosMonoNatOfIsOrderedAddMonoid` 📖	mathematical	—	`SMulPosMono` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `Nat.instPreorder` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`nsmul_le_nsmul_left` `IsOrderedAddMonoid.toAddLeftMono`
`instSMulPosStrictMonoIntOfIsOrderedAddMonoid` 📖	mathematical	—	`SMulPosStrictMono` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`zsmul_lt_zsmul_left`
`instSMulPosStrictMonoNatOfIsOrderedCancelAddMonoid` 📖	mathematical	—	`SMulPosStrictMono` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `Nat.instPreorder` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`nsmul_lt_nsmul_left` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid`
`inv_smul_le_iff_of_pos` 📖	mathematical	`Preorder.toLT` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`Preorder.toLE` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`smul_le_smul_iff_of_pos_left` `smul_inv_smul₀` `LT.lt.ne'`
`inv_smul_lt_iff_of_pos` 📖	mathematical	`Preorder.toLT` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`smul_lt_smul_iff_of_pos_left` `smul_inv_smul₀` `LT.lt.ne'`
`le_inv_smul_iff_of_pos` 📖	mathematical	`Preorder.toLT` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`Preorder.toLE` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`smul_le_smul_iff_of_pos_left` `smul_inv_smul₀` `LT.lt.ne'`
`le_of_smul_le_smul_left` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`PosSMulReflectLE.le_of_smul_le_smul_left`
`le_of_smul_le_smul_of_neg` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Preorder.toLT` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—	`le_of_smul_le_smul_of_pos_left` `neg_le_neg_iff` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `neg_smul` `neg_neg` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedRing.toIsOrderedAddMonoid`
`le_of_smul_le_smul_of_pos_left` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`le_of_smul_le_smul_left`
`le_of_smul_le_smul_of_pos_right` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`le_of_smul_le_smul_right`
`le_of_smul_le_smul_right` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`SMulPosReflectLE.le_of_smul_le_smul_right`
`le_smul_iff_one_le_left` 📖	mathematical	`Preorder.toLT`	`Preorder.toLE` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`one_smul` `smul_le_smul_iff_of_pos_right`
`le_smul_of_one_le_left` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`one_smul` `smul_le_smul_of_nonneg_right`
`lt_inv_smul_iff_of_pos` 📖	mathematical	`Preorder.toLT` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`smul_lt_smul_iff_of_pos_left` `smul_inv_smul₀` `LT.lt.ne'`
`lt_of_smul_lt_smul_left` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`PosSMulReflectLT.lt_of_smul_lt_smul_left`
`lt_of_smul_lt_smul_of_nonneg_left` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`lt_of_smul_lt_smul_left`
`lt_of_smul_lt_smul_of_nonneg_right` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`lt_of_smul_lt_smul_right`
`lt_of_smul_lt_smul_of_nonpos` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—	`lt_of_smul_lt_smul_of_nonneg_left` `neg_lt_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `neg_smul` `neg_neg` `neg_nonneg_of_nonpos` `IsOrderedRing.toIsOrderedAddMonoid`
`lt_of_smul_lt_smul_right` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`SMulPosReflectLT.lt_of_smul_lt_smul_right`
`lt_smul_iff_one_lt_left` 📖	mathematical	`Preorder.toLT`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`one_smul` `smul_lt_smul_iff_of_pos_right`
`lt_smul_of_one_lt_left` 📖	mathematical	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`one_smul` `smul_lt_smul_of_pos_right`
`monotone_smul_left_of_nonneg` 📖	mathematical	`Preorder.toLE`	`Monotone`	—	`PosSMulMono.smul_le_smul_of_nonneg_left`
`monotone_smul_right_of_nonneg` 📖	mathematical	`Preorder.toLE`	`Monotone`	—	`SMulPosMono.smul_le_smul_of_nonneg_right`
`neg_iff_neg_of_smul_pos` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	—	`neg_of_smul_pos_right` `le_of_lt` `neg_of_smul_pos_left`
`neg_of_smul_neg_left` 📖	—	`Preorder.toLT` `SMulZeroClass.toSMul` `Preorder.toLE`	—	—	`lt_of_smul_lt_smul_left` `smul_zero`
`neg_of_smul_neg_left'` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `Preorder.toLE`	—	—	`lt_of_not_ge` `LE.le.not_gt` `smul_nonneg'`
`neg_of_smul_neg_right` 📖	—	`Preorder.toLT` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `Preorder.toLE`	—	—	`lt_of_smul_lt_smul_right` `zero_smul`
`neg_of_smul_neg_right'` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `Preorder.toLE`	—	—	`lt_of_not_ge` `LE.le.not_gt` `smul_nonneg`
`neg_of_smul_pos_left` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `Preorder.toLE`	—	—	`pos_and_pos_or_neg_and_neg_of_smul_pos` `LT.lt.not_ge`
`neg_of_smul_pos_right` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `Preorder.toLE`	—	—	`pos_and_pos_or_neg_and_neg_of_smul_pos` `LT.lt.not_ge`
`nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`LE.le.not_gt` `lt_trichotomy` `smul_neg_of_pos_of_neg` `LT.lt.le` `LT.lt.asymm` `le_rfl` `smul_neg_of_neg_of_pos` `PosSMulStrictMono.toSMulPosStrictMono` `IsStrictOrderedRing.toIsOrderedRing`
`posSMulMono_iff_posSMulReflectLT` 📖	mathematical	—	`PosSMulMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `PosSMulReflectLT`	—	`PosSMulMono.toPosSMulReflectLT` `PosSMulReflectLT.toPosSMulMono`
`posSMulMono_iff_posSMulStrictMono` 📖	mathematical	—	`PosSMulMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `PosSMulStrictMono`	—	`PosSMulMono.toPosSMulStrictMono` `PosSMulStrictMono.toPosSMulMono`
`posSMulStrictMono_iff_PosSMulReflectLE` 📖	mathematical	—	`PosSMulStrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `PosSMulReflectLE`	—	`PosSMulStrictMono.toPosSMulReflectLE` `PosSMulReflectLE.toPosSMulStrictMono`
`pos_and_pos_or_neg_and_neg_of_smul_pos` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	—	`lt_trichotomy` `lt_imp_lt_of_le_imp_le` `smul_nonpos_of_nonpos_of_nonneg` `LT.lt.le` `LT.lt.false` `zero_smul` `smul_nonpos_of_nonneg_of_nonpos`
`pos_iff_pos_of_smul_pos` 📖	—	`Preorder.toLT` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	—	`pos_of_smul_pos_left` `le_of_lt` `pos_of_smul_pos_right`
`pos_of_smul_pos_left` 📖	—	`Preorder.toLT` `SMulZeroClass.toSMul` `Preorder.toLE`	—	—	`lt_of_smul_lt_smul_left` `smul_zero`
`pos_of_smul_pos_right` 📖	—	`Preorder.toLT` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `Preorder.toLE`	—	—	`lt_of_smul_lt_smul_right` `zero_smul`
`smulPosMono_iff_smulPosReflectLT` 📖	mathematical	—	`SMulPosMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SMulPosReflectLT`	—	`SMulPosMono.toSMulPosReflectLT` `SMulPosReflectLT.toSMulPosMono`
`smulPosMono_iff_smulPosStrictMono` 📖	mathematical	—	`SMulPosMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulPosStrictMono`	—	`SMulPosMono.toSMulPosStrictMono` `SMulPosStrictMono.toSMulPosMono`
`smulPosStrictMono_iff_SMulPosReflectLE` 📖	mathematical	—	`SMulPosStrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SMulPosReflectLE`	—	`SMulPosStrictMono.toSMulPosReflectLE` `SMulPosReflectLE.toSMulPosStrictMono`
`smul_add_smul_le_smul_add_smul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`exists_nonneg_add_of_le` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `add_smul` `add_left_comm` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `smul_le_smul_of_nonneg_left`
`smul_add_smul_le_smul_add_smul'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`add_comm` `smul_add_smul_le_smul_add_smul`
`smul_add_smul_lt_smul_add_smul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`lt_iff_exists_pos_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `add_smul` `add_left_comm` `add_lt_add_right` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `smul_lt_smul_of_pos_left`
`smul_add_smul_lt_smul_add_smul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`add_comm` `smul_add_smul_lt_smul_add_smul`
`smul_eq_smul_iff_eq_and_eq_of_pos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	`SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`Eq.not_lt` `LE.le.trans_lt` `smul_le_smul_of_nonneg_left` `PosSMulStrictMono.toPosSMulMono` `LT.lt.le` `smul_lt_smul_of_pos_right` `LT.lt.trans_le` `smul_lt_smul_of_pos_left` `smul_le_smul_of_nonneg_right` `SMulPosStrictMono.toSMulPosMono`
`smul_eq_smul_iff_eq_and_eq_of_pos'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	`SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`Eq.not_lt` `LT.lt.trans_le` `smul_lt_smul_of_pos_right` `smul_le_smul_of_nonneg_left` `PosSMulStrictMono.toPosSMulMono` `LT.lt.le` `LE.le.trans_lt` `smul_le_smul_of_nonneg_right` `SMulPosStrictMono.toSMulPosMono` `smul_lt_smul_of_pos_left`
`smul_le_iff_le_one_left` 📖	mathematical	`Preorder.toLT`	`Preorder.toLE` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`one_smul` `smul_le_smul_iff_of_pos_right`
`smul_le_of_le_one_left` 📖	mathematical	`Preorder.toLE` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`one_smul` `smul_le_smul_of_nonneg_right`
`smul_le_smul` 📖	—	`Preorder.toLE`	—	—	`LE.le.trans` `smul_le_smul_of_nonneg_left` `smul_le_smul_of_nonneg_right`
`smul_le_smul'` 📖	—	`Preorder.toLE`	—	—	`LE.le.trans` `smul_le_smul_of_nonneg_right` `smul_le_smul_of_nonneg_left`
`smul_le_smul_iff_of_neg_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Preorder.toLE` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`neg_neg` `neg_smul` `neg_le_neg_iff` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `smul_le_smul_iff_of_pos_left` `neg_pos_of_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedRing.toIsOrderedAddMonoid`
`smul_le_smul_iff_of_pos_left` 📖	mathematical	`Preorder.toLT`	`Preorder.toLE`	—	`le_of_smul_le_smul_left` `smul_le_smul_of_nonneg_left` `LT.lt.le`
`smul_le_smul_iff_of_pos_right` 📖	mathematical	`Preorder.toLT`	`Preorder.toLE`	—	`le_of_smul_le_smul_right` `smul_le_smul_of_nonneg_right` `LT.lt.le`
`smul_le_smul_of_nonneg_left` 📖	—	`Preorder.toLE`	—	—	`monotone_smul_left_of_nonneg`
`smul_le_smul_of_nonneg_right` 📖	—	`Preorder.toLE`	—	—	`monotone_smul_right_of_nonneg`
`smul_le_smul_of_nonpos_left` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`neg_neg` `neg_smul` `neg_le_neg_iff` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `smul_le_smul_of_nonneg_left` `neg_nonneg_of_nonpos` `IsOrderedRing.toIsOrderedAddMonoid`
`smul_lt_iff_lt_one_left` 📖	mathematical	`Preorder.toLT`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`one_smul` `smul_lt_smul_iff_of_pos_right`
`smul_lt_of_lt_one_left` 📖	mathematical	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`one_smul` `smul_lt_smul_of_pos_right`
`smul_lt_smul` 📖	—	`Preorder.toLT`	—	—	`LT.lt.trans` `smul_lt_smul_of_pos_left` `smul_lt_smul_of_pos_right`
`smul_lt_smul'` 📖	—	`Preorder.toLT`	—	—	`LT.lt.trans` `smul_lt_smul_of_pos_right` `smul_lt_smul_of_pos_left`
`smul_lt_smul_iff_of_neg_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`neg_neg` `neg_smul` `neg_lt_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `smul_lt_smul_iff_of_pos_left` `neg_pos_of_neg` `IsOrderedRing.toIsOrderedAddMonoid`
`smul_lt_smul_iff_of_pos_left` 📖	—	`Preorder.toLT`	—	—	`lt_of_smul_lt_smul_left` `LT.lt.le` `smul_lt_smul_of_pos_left`
`smul_lt_smul_iff_of_pos_right` 📖	—	`Preorder.toLT`	—	—	`lt_of_smul_lt_smul_right` `LT.lt.le` `smul_lt_smul_of_pos_right`
`smul_lt_smul_of_le_of_lt` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`LT.lt.trans_le` `smul_lt_smul_of_pos_left` `smul_le_smul_of_nonneg_right`
`smul_lt_smul_of_le_of_lt'` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`LE.le.trans_lt` `smul_le_smul_of_nonneg_right` `smul_lt_smul_of_pos_left`
`smul_lt_smul_of_lt_of_le` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`LE.le.trans_lt` `smul_le_smul_of_nonneg_left` `smul_lt_smul_of_pos_right`
`smul_lt_smul_of_lt_of_le'` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`LT.lt.trans_le` `smul_lt_smul_of_pos_right` `smul_le_smul_of_nonneg_left`
`smul_lt_smul_of_neg_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`neg_neg` `neg_smul` `neg_lt_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `smul_lt_smul_of_pos_left` `neg_pos_of_neg` `IsOrderedRing.toIsOrderedAddMonoid`
`smul_lt_smul_of_pos_left` 📖	—	`Preorder.toLT`	—	—	`strictMono_smul_left_of_pos`
`smul_lt_smul_of_pos_right` 📖	—	`Preorder.toLT`	—	—	`strictMono_smul_right_of_pos`
`smul_max_of_nonneg` 📖	mathematical	`Preorder.toLE`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Monotone.map_max` `monotone_smul_left_of_nonneg`
`smul_max_of_nonpos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`Antitone.map_max` `antitone_smul_left`
`smul_min_of_nonneg` 📖	mathematical	`Preorder.toLE`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Monotone.map_min` `monotone_smul_left_of_nonneg`
`smul_min_of_nonpos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`Antitone.map_min` `antitone_smul_left`
`smul_neg_iff_of_neg_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`smul_zero` `smul_lt_smul_iff_of_neg_left`
`smul_neg_iff_of_pos_left` 📖	mathematical	`Preorder.toLT`	`SMulZeroClass.toSMul`	—	`smul_zero` `smul_lt_smul_iff_of_pos_left`
`smul_neg_of_neg_of_pos` 📖	mathematical	`Preorder.toLT`	`SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`zero_smul` `smul_lt_smul_of_pos_right`
`smul_neg_of_pos_of_neg` 📖	mathematical	`Preorder.toLT`	`SMulZeroClass.toSMul`	—	`smul_zero` `smul_lt_smul_of_pos_left`
`smul_nonneg` 📖	mathematical	`Preorder.toLE`	`SMulZeroClass.toSMul`	—	`smul_zero` `smul_le_smul_of_nonneg_left`
`smul_nonneg'` 📖	mathematical	`Preorder.toLE`	`SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`zero_smul` `smul_le_smul_of_nonneg_right`
`smul_nonneg_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg` `smul_nonneg` `PosSMulStrictMono.toPosSMulMono` `smul_nonneg_of_nonpos_of_nonpos` `PosSMulMono.toSMulPosMono` `IsStrictOrderedRing.toIsOrderedRing`
`smul_nonneg_iff_neg_imp_nonpos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`neg_smul_neg` `smul_nonneg_iff_pos_imp_nonneg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`smul_nonneg_iff_pos_imp_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`smul_nonneg_iff`
`smul_nonneg_of_nonpos_of_nonpos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_nonpos_of_nonpos_of_nonneg` `OrderDual.instSMulPosMono`
`smul_nonpos_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`neg_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `smul_neg` `smul_nonneg_iff` `neg_nonpos`
`smul_nonpos_iff_neg_imp_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`neg_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `neg_smul` `smul_nonneg_iff_pos_imp_nonneg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`smul_nonpos_iff_pos_imp_nonpos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`neg_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `smul_neg` `smul_nonneg_iff_pos_imp_nonneg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`smul_nonpos_of_nonneg_of_nonpos` 📖	mathematical	`Preorder.toLE`	`SMulZeroClass.toSMul`	—	`smul_zero` `smul_le_smul_of_nonneg_left`
`smul_nonpos_of_nonpos_of_nonneg` 📖	mathematical	`Preorder.toLE`	`SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`zero_smul` `smul_le_smul_of_nonneg_right`
`smul_pos` 📖	mathematical	`Preorder.toLT`	`SMulZeroClass.toSMul`	—	`smul_zero` `smul_lt_smul_of_pos_left`
`smul_pos'` 📖	mathematical	`Preorder.toLT`	`SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`zero_smul` `smul_lt_smul_of_pos_right`
`smul_pos_iff_of_neg_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_zero` `smul_lt_smul_iff_of_neg_left`
`smul_pos_iff_of_pos_left` 📖	mathematical	`Preorder.toLT`	`SMulZeroClass.toSMul`	—	`smul_zero` `smul_lt_smul_iff_of_pos_left`
`smul_pos_iff_of_pos_right` 📖	mathematical	`Preorder.toLT`	`SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`zero_smul` `smul_lt_smul_iff_of_pos_right`
`smul_pos_of_neg_of_neg` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_pos_iff_of_neg_left`
`strictAnti_smul_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`StrictAnti` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_lt_smul_of_neg_left`
`strictMono_smul_left_of_pos` 📖	mathematical	`Preorder.toLT`	`StrictMono`	—	`PosSMulStrictMono.smul_lt_smul_of_pos_left`
`strictMono_smul_right_of_pos` 📖	mathematical	`Preorder.toLT`	`StrictMono`	—	`SMulPosStrictMono.smul_lt_smul_of_pos_right`

---

← Back to Index