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 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	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 instZero 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 instZero 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 instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_le_neg_iff addLeftMono IsOrderedAddMonoid.toAddLeftMono addRightMono covariant_swap_add_of_covariant_add 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 instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	le_of_smul_le_smul_right smul_neg neg_le_neg_iff addLeftMono IsOrderedAddMonoid.toAddLeftMono addRightMono covariant_swap_add_of_covariant_add neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
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 instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	lt_of_smul_lt_smul_right smul_neg neg_lt_neg_iff addLeftStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono addRightStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsOrderedCancelAddMonoid.toAddLeftReflectLT 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 instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_lt_neg_iff addLeftStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono addRightStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsOrderedCancelAddMonoid.toAddLeftReflectLT covariant_swap_add_of_covariant_add 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 GroupWithZero.toMonoidWithZero 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 GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	—

OrderedSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPosSMulMonoNat 📖	mathematical	—	PosSMulMono AddMonoid.toNSMul 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.toNSMul 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	PosSMulMono instSMul preorder	—	smul_le_smul_of_nonneg_left
instPosSMulReflectLE 📖	mathematical	PosSMulReflectLE	PosSMulReflectLE instSMul preorder	—	le_of_smul_le_smul_left
instPosSMulStrictMono 📖	mathematical	PosSMulStrictMono SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass PartialOrder.toPreorder	PosSMulStrictMono instSMul SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass PartialOrder.toPreorder preorder	—	smul_le_smul_of_nonneg_left instPosSMulMono PosSMulStrictMono.toPosSMulMono LT.lt.le smul_lt_smul_of_pos_left
instSMulPosMono 📖	mathematical	SMulPosMono	SMulPosMono instSMul preorder instZero	—	smul_le_smul_of_nonneg_right
instSMulPosReflectLE 📖	mathematical	SMulPosReflectLE	SMulPosReflectLE instSMul preorder instZero	—	lt_def le_of_smul_le_smul_right
instSMulPosReflectLT 📖	mathematical	SMulPosReflectLT SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass PartialOrder.toPreorder	SMulPosReflectLT instSMul SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass PartialOrder.toPreorder preorder instZero	—	lt_of_smul_lt_smul_right
instSMulPosStrictMono 📖	mathematical	SMulPosStrictMono SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass PartialOrder.toPreorder	SMulPosStrictMono instSMul SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass PartialOrder.toPreorder 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 SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass PartialOrder.toPreorder	—	LE.le.eq_or_lt zero_smul instReflLe
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 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	—	covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono smul_sub
smul_le_smul_of_nonneg_left 📖	mathematical	Preorder.toLE	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 📖	mathematical	Preorder.toLT Preorder.toLE	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 📖	mathematical	Preorder.toLE Preorder.toLT	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 📖	mathematical	Preorder.toLT	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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedCancelAddMonoid.toAddLeftReflectLT 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 SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass PartialOrder.toPreorder	—	LE.le.eq_or_lt smul_zero instReflLe
smul_le_smul_of_nonneg_right 📖	mathematical	Preorder.toLE	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 📖	mathematical	Preorder.toLT Preorder.toLE	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 📖	mathematical	Preorder.toLE Preorder.toLT	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 📖	mathematical	Preorder.toLT	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.toNSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.instPreorder PartialOrder.toPreorder MulZeroClass.toZero Nat.instMulZeroClass	—	nsmul_right_strictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsOrderedCancelAddMonoid.toAddLeftReflectLT covariant_swap_add_of_covariant_add LT.lt.ne'
toSMulPosStrictMonoNat 📖	mathematical	—	SMulPosStrictMono AddMonoid.toNSMul 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE 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	17 math math: IsOrderedModule.toPosSMulMono, OrderDual.instPosSMulMono, PosSMulStrictMono.toPosSMulMono, PosSMulMono.lift, PosSMulMono.of_pos, PosSMulMono.nnrat_of_rat, OrderedSemiring.toPosSMulMonoNat, instPosSMulMonoNatOfIsOrderedAddMonoid, PosSMulReflectLT.toPosSMulMono, DFinsupp.instPosSMulMono, posSMulMono_iff_posSMulReflectLT, Pi.instPosSMulMono, Finsupp.instPosSMulMono, PosMulMono.toPosSMulMono, Prod.instPosSMulMono, posSMulMono_iff_posSMulStrictMono, PosSMulMono.of_smul_nonneg
PosSMulReflectLE 📖	CompData	12 math math: Finsupp.instPosSMulReflectLE, PosSMulReflectLE_iff_posSMulReflectLT, OrderDual.instPosSMulReflectLE, Prod.instPosSMulReflectLE, posSMulStrictMono_iff_PosSMulReflectLE, PosMulReflectLE.toPosSMulReflectLE, Pi.instPosSMulReflectLE, PosSMulStrictMono.toPosSMulReflectLE, DFinsupp.instPosSMulReflectLE, PosSMulReflectLT.toPosSMulReflectLE, PosSMulReflectLE.lift, PosSMulMono.toPosSMulReflectLE
PosSMulReflectLT 📖	CompData	9 math math: PosSMulReflectLE_iff_posSMulReflectLT, PosSMulReflectLT.of_pos, PosSMulReflectLT.lift, OrderDual.instPosSMulReflectLT, posSMulMono_iff_posSMulReflectLT, PosMulReflectLT.toPosSMulReflectLT, PosSMulReflectLE.toPosSMulReflectLT, PosSMulMono.toPosSMulReflectLT, PosSMulStrictMono.toPosSMulReflectLT
PosSMulStrictMono 📖	CompData	21 math math: instPosSMulStrictMonoIntOfIsOrderedAddMonoid, IsStrictOrderedModule.toPosSMulStrictMono, Pi.instPosSMulStrictMono, NNReal.instPosSMulStrictMono, posSMulStrictMono_iff_PosSMulReflectLE, instPosSMulStrictMono, DFinsupp.instPosSMulStrictMono, 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	17 math math: MulPosMono.toSMulPosMono, smulPosMono_iff_smulPosStrictMono, SMulPosMono.lift, DFinsupp.instSMulPosMono, IsOrderedModule.toSMulPosMono, ENNReal.instSMulPosMonoNNReal, SMulPosStrictMono.toSMulPosMono, SMulPosMono.of_pos, Finsupp.instSMulPosMono, OrderDual.instSMulPosMono, PosSMulMono.toSMulPosMono, OrderedSemiring.toSMulPosMonoNat, SMulPosReflectLT.toSMulPosMono, Pi.instSMulPosMono, instSMulPosMonoNatOfIsOrderedAddMonoid, smulPosMono_iff_smulPosReflectLT, Prod.instSMulPosMono
SMulPosReflectLE 📖	CompData	11 math math: Finsupp.instSMulPosReflectLE, SMulPosReflectLE_iff_smulPosReflectLT, smulPosStrictMono_iff_SMulPosReflectLE, OrderDual.instSMulPosReflectLE, SMulPosReflectLT.toSMulPosReflectLE, SMulPosReflectLE.lift, MulPosReflectLE.toSMulPosReflectLE, Prod.instSMulPosReflectLE, SMulPosStrictMono.toSMulPosReflectLE, DFinsupp.instSMulPosReflectLE, Pi.instSMulPosReflectLE
SMulPosReflectLT 📖	CompData	12 math math: SMulPosReflectLE_iff_smulPosReflectLT, SMulPosMono.toSMulPosReflectLT, Finsupp.instSMulPosReflectLT, SMulPosReflectLT.lift, MulPosReflectLT.toSMulPosReflectLT, Pi.instSMulPosReflectLT, OrderDual.instSMulPosReflectLT, DFinsupp.instSMulPosReflectLT, SMulPosReflectLE.toSMulPosReflectLT, SMulPosReflectLT.of_pos, Prod.instSMulPosReflectLT, smulPosMono_iff_smulPosReflectLT
SMulPosStrictMono 📖	CompData	17 math math: smulPosMono_iff_smulPosStrictMono, smulPosStrictMono_iff_SMulPosReflectLE, OrderDual.instSMulPosStrictMono, SMulPosStrictMono.lift, Pi.instSMulPosStrictMono, MulPosStrictMono.toSMulPosStrictMono, StrictOrderedSemiring.toSMulPosStrictMonoNat, Prod.instSMulPosStrictMono, Finsupp.instSMulPosStrictMono, instSMulPosStrictMonoIntOfIsOrderedAddMonoid, instSMulPosStrictMonoNatOfIsOrderedCancelAddMonoid, SMulPosMono.toSMulPosStrictMono, NNReal.instSMulPosStrictMono, SMulPosReflectLE.toSMulPosStrictMono, PosSMulStrictMono.toSMulPosStrictMono, IsStrictOrderedModule.toSMulPosStrictMono, DFinsupp.instSMulPosStrictMono

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 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	—	smul_le_smul_of_nonpos_left
instPosSMulMonoNatOfIsOrderedAddMonoid 📖	mathematical	—	PosSMulMono AddMonoid.toNSMul 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.toNSMul 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.toNSMul 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.toNSMul AddCommMonoid.toAddMonoid Nat.instPreorder PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	nsmul_lt_nsmul_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE 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 GroupWithZero.toMonoidWithZero 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	Preorder.toLT SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero 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 GroupWithZero.toMonoidWithZero 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 📖	mathematical	Preorder.toLE Preorder.toLT	Preorder.toLE	—	PosSMulReflectLE.le_of_smul_le_smul_left
le_of_smul_le_smul_of_neg 📖	mathematical	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	Preorder.toLE PartialOrder.toPreorder	—	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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedRing.toIsOrderedAddMonoid
le_of_smul_le_smul_of_pos_left 📖	mathematical	Preorder.toLE Preorder.toLT	Preorder.toLE	—	le_of_smul_le_smul_left
le_of_smul_le_smul_of_pos_right 📖	mathematical	Preorder.toLE Preorder.toLT	Preorder.toLE	—	le_of_smul_le_smul_right
le_of_smul_le_smul_right 📖	mathematical	Preorder.toLE Preorder.toLT	Preorder.toLE	—	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	Preorder.toLE 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	Preorder.toLT SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero 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 📖	mathematical	Preorder.toLT Preorder.toLE	Preorder.toLT	—	PosSMulReflectLT.lt_of_smul_lt_smul_left
lt_of_smul_lt_smul_of_nonneg_left 📖	mathematical	Preorder.toLT Preorder.toLE	Preorder.toLT	—	lt_of_smul_lt_smul_left
lt_of_smul_lt_smul_of_nonneg_right 📖	mathematical	Preorder.toLT Preorder.toLE	Preorder.toLT	—	lt_of_smul_lt_smul_right
lt_of_smul_lt_smul_of_nonpos 📖	mathematical	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	Preorder.toLT PartialOrder.toPreorder	—	lt_of_smul_lt_smul_of_nonneg_left neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsOrderedCancelAddMonoid.toAddLeftReflectLT covariant_swap_add_of_covariant_add neg_smul neg_neg neg_nonneg_of_nonpos IsOrderedRing.toIsOrderedAddMonoid
lt_of_smul_lt_smul_right 📖	mathematical	Preorder.toLT Preorder.toLE	Preorder.toLT	—	SMulPosReflectLT.lt_of_smul_lt_smul_right
lt_smul_iff_one_lt_left 📖	mathematical	Preorder.toLT	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	Preorder.toLT 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 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	neg_of_smul_pos_right le_of_lt neg_of_smul_pos_left
neg_of_smul_neg_left 📖	mathematical	Preorder.toLT SMulZeroClass.toSMul Preorder.toLE	Preorder.toLT	—	lt_of_smul_lt_smul_left smul_zero
neg_of_smul_neg_left' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass Preorder.toLE	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	lt_of_not_ge LE.le.not_gt smul_nonneg'
neg_of_smul_neg_right 📖	mathematical	Preorder.toLT SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass Preorder.toLE	Preorder.toLT	—	lt_of_smul_lt_smul_right zero_smul
neg_of_smul_neg_right' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass Preorder.toLE	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	lt_of_not_ge LE.le.not_gt smul_nonneg
neg_of_smul_pos_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass Preorder.toLE	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	pos_and_pos_or_neg_and_neg_of_smul_pos LT.lt.not_ge
neg_of_smul_pos_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass Preorder.toLE	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	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 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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 📖	mathematical	Preorder.toLT SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass	Preorder.toLT	—	pos_of_smul_pos_left le_of_lt pos_of_smul_pos_right
pos_of_smul_pos_left 📖	mathematical	Preorder.toLT SMulZeroClass.toSMul Preorder.toLE	Preorder.toLT	—	lt_of_smul_lt_smul_left smul_zero
pos_of_smul_pos_right 📖	mathematical	Preorder.toLT SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass Preorder.toLE	Preorder.toLT	—	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	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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE 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	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	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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE 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	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	Preorder.toLE SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	one_smul smul_le_smul_of_nonneg_right
smul_le_smul 📖	mathematical	Preorder.toLE	Preorder.toLE	—	LE.le.trans smul_le_smul_of_nonneg_left smul_le_smul_of_nonneg_right
smul_le_smul' 📖	mathematical	Preorder.toLE	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 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	—	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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid 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 📖	mathematical	Preorder.toLE	Preorder.toLE	—	monotone_smul_left_of_nonneg
smul_le_smul_of_nonneg_right 📖	mathematical	Preorder.toLE	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	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	—	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	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	Preorder.toLT SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	one_smul smul_lt_smul_of_pos_right
smul_lt_smul 📖	mathematical	Preorder.toLT	Preorder.toLT	—	LT.lt.trans smul_lt_smul_of_pos_left smul_lt_smul_of_pos_right
smul_lt_smul' 📖	mathematical	Preorder.toLT	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	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	—	neg_neg neg_smul neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsOrderedCancelAddMonoid.toAddLeftReflectLT 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 📖	mathematical	Preorder.toLT	Preorder.toLT	—	lt_of_smul_lt_smul_left LT.lt.le smul_lt_smul_of_pos_left
smul_lt_smul_iff_of_pos_right 📖	mathematical	Preorder.toLT	Preorder.toLT	—	lt_of_smul_lt_smul_right LT.lt.le smul_lt_smul_of_pos_right
smul_lt_smul_of_le_of_lt 📖	mathematical	Preorder.toLE Preorder.toLT	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' 📖	mathematical	Preorder.toLE Preorder.toLT	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 📖	mathematical	Preorder.toLT Preorder.toLE	Preorder.toLT	—	LE.le.trans_lt smul_le_smul_of_nonneg_left smul_lt_smul_of_pos_right
smul_lt_smul_of_lt_of_le' 📖	mathematical	Preorder.toLT Preorder.toLE	Preorder.toLT	—	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	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	—	neg_neg neg_smul neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsOrderedCancelAddMonoid.toAddLeftReflectLT covariant_swap_add_of_covariant_add smul_lt_smul_of_pos_left neg_pos_of_neg IsOrderedRing.toIsOrderedAddMonoid
smul_lt_smul_of_pos_left 📖	mathematical	Preorder.toLT	Preorder.toLT	—	strictMono_smul_left_of_pos
smul_lt_smul_of_pos_right 📖	mathematical	Preorder.toLT	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	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 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	Preorder.toLT SMulZeroClass.toSMul	—	smul_zero smul_lt_smul_iff_of_pos_left
smul_neg_of_neg_of_pos 📖	mathematical	Preorder.toLT	Preorder.toLT SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass	—	zero_smul smul_lt_smul_of_pos_right
smul_neg_of_pos_of_neg 📖	mathematical	Preorder.toLT	Preorder.toLT SMulZeroClass.toSMul	—	smul_zero smul_lt_smul_of_pos_left
smul_nonneg 📖	mathematical	Preorder.toLE	Preorder.toLE SMulZeroClass.toSMul	—	smul_zero smul_le_smul_of_nonneg_left
smul_nonneg' 📖	mathematical	Preorder.toLE	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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
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	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	—	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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
smul_nonpos_of_nonneg_of_nonpos 📖	mathematical	Preorder.toLE	Preorder.toLE SMulZeroClass.toSMul	—	smul_zero smul_le_smul_of_nonneg_left
smul_nonpos_of_nonpos_of_nonneg 📖	mathematical	Preorder.toLE	Preorder.toLE SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass	—	zero_smul smul_le_smul_of_nonneg_right
smul_pos 📖	mathematical	Preorder.toLT	Preorder.toLT SMulZeroClass.toSMul	—	smul_zero smul_lt_smul_of_pos_left
smul_pos' 📖	mathematical	Preorder.toLT	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	Preorder.toLT 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	—	smul_zero smul_lt_smul_iff_of_neg_left
smul_pos_iff_of_pos_left 📖	mathematical	Preorder.toLT	Preorder.toLT SMulZeroClass.toSMul	—	smul_zero smul_lt_smul_iff_of_pos_left
smul_pos_iff_of_pos_right 📖	mathematical	Preorder.toLT	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	Preorder.toLT 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	—	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 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	—	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