Defs

📁 Source: Mathlib/Algebra/Order/GroupWithZero/Unbundled/Defs.lean

Statistics

Metric	Count
Definitions `MulPosMono`, `MulPosReflectLE`, `MulPosReflectLT`, `MulPosStrictMono`, `PosMulMono`, `PosMulReflectLE`, `PosMulReflectLT`, `PosMulStrictMono`	8
Theorems `mulPosMono`, `mulPosStrictMono`, `posMulMono`, `posMulStrictMono`, `toPosMulMono`, `toPosMulReflectLT`, `toPosMulReflectLE`, `toPosMulStrictMono`, `mul_le_mul_of_nonneg_right`, `toMulPosReflectLT`, `to_covariantClass_nonneg_mul_le`, `to_covariantClass_pos_mul_le`, `toContravariantClass`, `toMulPosStrictMono`, `toContravariantClass`, `toMulPosMono`, `to_contravariantClass_pos_mul_lt`, `mul_lt_mul_of_pos_right`, `toMulPosReflectLE`, `to_covariantClass_pos_mul_le`, `toMulPosMono`, `toMulPosReflectLT`, `toMulPosReflectLE`, `toMulPosStrictMono`, `mul_le_mul_of_nonneg_left`, `toMulPosMono`, `toPosMulReflectLT`, `to_covariantClass_nonneg_mul_le`, `to_covariantClass_pos_mul_le`, `toContravariantClass`, `toMulPosReflectLE`, `toPosMulStrictMono`, `toContravariantClass`, `toMulPosReflectLT`, `toPosMulMono`, `to_contravariantClass_pos_mul_lt`, `mul_lt_mul_of_pos_left`, `toMulPosStrictMono`, `toPosMulReflectLE`, `to_covariantClass_pos_mul_le`, `le_mul_of_le_mul_of_nonneg_left`, `le_mul_of_le_mul_of_nonneg_right`, `le_of_mul_le_mul_left`, `le_of_mul_le_mul_of_pos_left`, `le_of_mul_le_mul_of_pos_right`, `le_of_mul_le_mul_right`, `lt_mul_of_lt_mul_of_nonneg_left`, `lt_mul_of_lt_mul_of_nonneg_right`, `lt_of_mul_lt_mul_left`, `lt_of_mul_lt_mul_of_nonneg_left`, `lt_of_mul_lt_mul_of_nonneg_right`, `lt_of_mul_lt_mul_right`, `mulPosMono_iff`, `mulPosMono_iff_mulPosReflectLT`, `mulPosReflectLE_iff`, `mulPosReflectLT_iff`, `mulPosStrictMono_iff`, `mulPosStrictMono_iff_mulPosReflectLE`, `mul_le_mul`, `mul_le_mul_iff_left₀`, `mul_le_mul_iff_of_pos_left`, `mul_le_mul_iff_of_pos_right`, `mul_le_mul_iff_right₀`, `mul_le_mul_of_nonneg`, `mul_le_mul_of_nonneg'`, `mul_le_mul_of_nonneg_left`, `mul_le_mul_of_nonneg_right`, `mul_le_of_mul_le_of_nonneg_left`, `mul_le_of_mul_le_of_nonneg_right`, `mul_lt_mul`, `mul_lt_mul'`, `mul_lt_mul_iff_left₀`, `mul_lt_mul_iff_of_pos_left`, `mul_lt_mul_iff_of_pos_right`, `mul_lt_mul_iff_right₀`, `mul_lt_mul_of_le_of_lt_of_nonneg_of_pos`, `mul_lt_mul_of_le_of_lt_of_pos_of_nonneg`, `mul_lt_mul_of_lt_of_le_of_nonneg_of_pos`, `mul_lt_mul_of_lt_of_le_of_pos_of_nonneg`, `mul_lt_mul_of_nonneg_of_pos`, `mul_lt_mul_of_nonneg_of_pos'`, `mul_lt_mul_of_pos`, `mul_lt_mul_of_pos'`, `mul_lt_mul_of_pos_left`, `mul_lt_mul_of_pos_of_nonneg`, `mul_lt_mul_of_pos_of_nonneg'`, `mul_lt_mul_of_pos_right`, `mul_lt_of_mul_lt_of_nonneg_left`, `mul_lt_of_mul_lt_of_nonneg_right`, `posMulMono_iff`, `posMulMono_iff_mulPosMono`, `posMulMono_iff_posMulReflectLT`, `posMulReflectLE_iff`, `posMulReflectLE_iff_mulPosReflectLE`, `posMulReflectLT_iff`, `posMulReflectLT_iff_mulPosReflectLT`, `posMulStrictMono_iff`, `posMulStrictMono_iff_mulPosStrictMono`, `posMulStrictMono_iff_posMulReflectLE`	99
Total	107

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulPosMono` 📖	mathematical	`Preorder.toLE`	`MulPosMono`	—	`mul_le_mul_of_nonneg_right`
`mulPosStrictMono` 📖	mathematical	`Preorder.toLT`	`MulPosStrictMono`	—	`mul_lt_mul_of_pos_right`
`posMulMono` 📖	mathematical	`Preorder.toLE`	`PosMulMono`	—	`mul_le_mul_of_nonneg_left`
`posMulStrictMono` 📖	mathematical	`Preorder.toLT`	`PosMulStrictMono`	—	`mul_lt_mul_of_pos_left`

MulLeftMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPosMulMono` 📖	mathematical	—	`PosMulMono`	—	`CovariantClass.elim`
`toPosMulReflectLT` 📖	mathematical	—	`PosMulReflectLT`	—	`ContravariantClass.elim`

MulLeftStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPosMulReflectLE` 📖	mathematical	—	`PosMulReflectLE`	—	`ContravariantClass.elim`
`toPosMulStrictMono` 📖	mathematical	—	`PosMulStrictMono`	—	`CovariantClass.elim`

MulPosMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_le_mul_of_nonneg_right` 📖	—	`Preorder.toLE`	—	—	—
`toMulPosReflectLT` 📖	mathematical	—	`MulPosReflectLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`covariant_le_iff_contravariant_lt` `mul_le_mul_of_nonneg_right`
`to_covariantClass_nonneg_mul_le` 📖	mathematical	—	`CovariantClass` `Preorder.toLE`	—	`mul_le_mul_of_nonneg_right`
`to_covariantClass_pos_mul_le` 📖	mathematical	—	`CovariantClass` `Preorder.toLT` `Preorder.toLE`	—	`mul_le_mul_of_nonneg_right` `LT.lt.le`

MulPosReflectLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toContravariantClass` 📖	mathematical	—	`ContravariantClass` `Preorder.toLT` `Preorder.toLE`	—	—
`toMulPosStrictMono` 📖	mathematical	—	`MulPosStrictMono` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`not_le` `LT.lt.not_ge` `le_of_mul_le_mul_right`

MulPosReflectLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toContravariantClass` 📖	mathematical	—	`ContravariantClass` `Preorder.toLE` `Preorder.toLT`	—	—
`toMulPosMono` 📖	mathematical	—	`MulPosMono` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`not_lt` `LE.le.not_gt` `lt_of_mul_lt_mul_right`
`to_contravariantClass_pos_mul_lt` 📖	mathematical	—	`ContravariantClass` `Preorder.toLT`	—	`ContravariantClass.elim` `toContravariantClass` `LT.lt.le`

MulPosStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_lt_mul_of_pos_right` 📖	—	`Preorder.toLT`	—	—	—
`toMulPosReflectLE` 📖	mathematical	—	`MulPosReflectLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`covariant_lt_iff_contravariant_le` `CovariantClass.elim` `to_covariantClass_pos_mul_le`
`to_covariantClass_pos_mul_le` 📖	mathematical	—	`CovariantClass` `Preorder.toLT`	—	`mul_lt_mul_of_pos_right`

MulRightMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMulPosMono` 📖	mathematical	—	`MulPosMono`	—	`CovariantClass.elim`
`toMulPosReflectLT` 📖	mathematical	—	`MulPosReflectLT`	—	`ContravariantClass.elim`

MulRightStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMulPosReflectLE` 📖	mathematical	—	`MulPosReflectLE`	—	`ContravariantClass.elim`
`toMulPosStrictMono` 📖	mathematical	—	`MulPosStrictMono`	—	`CovariantClass.elim`

PosMulMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_le_mul_of_nonneg_left` 📖	—	`Preorder.toLE`	—	—	—
`toMulPosMono` 📖	mathematical	—	`MulPosMono`	—	`posMulMono_iff_mulPosMono`
`toPosMulReflectLT` 📖	mathematical	—	`PosMulReflectLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`covariant_le_iff_contravariant_lt` `mul_le_mul_of_nonneg_left`
`to_covariantClass_nonneg_mul_le` 📖	mathematical	—	`CovariantClass` `Preorder.toLE`	—	`mul_le_mul_of_nonneg_left`
`to_covariantClass_pos_mul_le` 📖	mathematical	—	`CovariantClass` `Preorder.toLT` `Preorder.toLE`	—	`mul_le_mul_of_nonneg_left` `LT.lt.le`

PosMulReflectLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toContravariantClass` 📖	mathematical	—	`ContravariantClass` `Preorder.toLT` `Preorder.toLE`	—	—
`toMulPosReflectLE` 📖	mathematical	—	`MulPosReflectLE`	—	`posMulReflectLE_iff_mulPosReflectLE`
`toPosMulStrictMono` 📖	mathematical	—	`PosMulStrictMono` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`not_le` `LT.lt.not_ge` `le_of_mul_le_mul_left`

PosMulReflectLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toContravariantClass` 📖	mathematical	—	`ContravariantClass` `Preorder.toLE` `Preorder.toLT`	—	—
`toMulPosReflectLT` 📖	mathematical	—	`MulPosReflectLT`	—	`posMulReflectLT_iff_mulPosReflectLT`
`toPosMulMono` 📖	mathematical	—	`PosMulMono` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`not_lt` `LE.le.not_gt` `lt_of_mul_lt_mul_left`
`to_contravariantClass_pos_mul_lt` 📖	mathematical	—	`ContravariantClass` `Preorder.toLT`	—	`ContravariantClass.elim` `toContravariantClass` `LT.lt.le`

PosMulStrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_lt_mul_of_pos_left` 📖	—	`Preorder.toLT`	—	—	—
`toMulPosStrictMono` 📖	mathematical	—	`MulPosStrictMono`	—	`posMulStrictMono_iff_mulPosStrictMono`
`toPosMulReflectLE` 📖	mathematical	—	`PosMulReflectLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	—	`covariant_lt_iff_contravariant_le` `CovariantClass.elim` `to_covariantClass_pos_mul_le`
`to_covariantClass_pos_mul_le` 📖	mathematical	—	`CovariantClass` `Preorder.toLT`	—	`mul_lt_mul_of_pos_left`

(root)

Definitions

Name	Category	Theorems
`MulPosMono` 📖	CompData	14 math math: `PosMulMono.toMulPosMono`, `WithBot.instMulPosMono`, `mulPosMono_iff_covariant_pos`, `EReal.instMulPosMono`, `MulPosStrictMono.toMulPosMono`, `MulRightMono.toMulPosMono`, `mulPosMono_iff`, `Function.Injective.mulPosMono`, `mulPosMono_iff_mulPosReflectLT`, `posMulMono_iff_mulPosMono`, `instMulPosMonoWithZeroOfMulRightMono`, `MulPosReflectLT.toMulPosMono`, `IsOrderedRing.toMulPosMono`, `mulPosMono_iff_mulPosStrictMono`
`MulPosReflectLE` 📖	CompData	12 math math: `PosMulReflectLE.toMulPosReflectLE`, `FractionalIdeal.instMulPosReflectLENonZeroDivisors`, `MulRightStrictMono.toMulPosReflectLE`, `RCLike.instMulPosReflectLE`, `mulPosStrictMono_iff_mulPosReflectLE`, `MulPosReflectLE.of_posMulReflectLT_of_mulPosMono`, `mulPosReflectLE_iff_mulPosReflectLT`, `mulPosReflectLE_iff`, `posMulReflectLE_iff_mulPosReflectLE`, `WithBot.instMulPosReflectLE`, `MulPosStrictMono.toMulPosReflectLE`, `MulPosReflectLT.toMulPosReflectLE`
`MulPosReflectLT` 📖	CompData	11 math math: `mulPosReflectLT_iff`, `MulPosReflectLE.toMulPosReflectLT`, `mulPosMono_iff_mulPosReflectLT`, `mulPosReflectLE_iff_mulPosReflectLT`, `EReal.instMulPosReflectLT`, `posMulReflectLT_iff_mulPosReflectLT`, `WithBot.instMulPosReflectLT`, `mulPosReflectLT_iff_contravariant_pos`, `PosMulReflectLT.toMulPosReflectLT`, `MulRightMono.toMulPosReflectLT`, `MulPosMono.toMulPosReflectLT`
`MulPosStrictMono` 📖	CompData	17 math math: `FractionalIdeal.instMulPosStrictMonoNonZeroDivisors`, `IsStrictOrderedRing.toMulPosStrictMono`, `MulPosMono.toMulPosStrictMono`, `MulPosReflectLE.toMulPosStrictMono`, `Function.Injective.mulPosStrictMono`, `WithBot.instMulPosStrictMono`, `mulPosStrictMono_iff_mulPosReflectLE`, `MulPosReflectLT.toMulPosStrictMono`, `mulPosStrictMono_iff`, `PosMulStrictMono.toMulPosStrictMono`, `posMulStrictMono_iff_mulPosStrictMono`, `MulRightStrictMono.toMulPosStrictMono`, `instMulPosStrictMonoIdeal`, `LinearOrderedCommMonoidWithZero.toMulPosStrictMono`, `instMulPosStrictMonoWithZeroOfMulRightStrictMono`, `ConditionallyCompleteLinearOrderedField.toMulPosStrictMono`, `mulPosMono_iff_mulPosStrictMono`
`PosMulMono` 📖	CompData	14 math math: `instPosMulMonoWithZeroOfMulLeftMono`, `IsOrderedRing.toPosMulMono`, `posMulMono_iff_covariant_pos`, `EReal.instPosMulMono`, `Function.Injective.posMulMono`, `PosMulReflectLT.toPosMulMono`, `Rat.instPosMulMono`, `WithBot.instPosMulMono`, `posMulMono_iff_mulPosMono`, `posMulMono_iff`, `PosMulStrictMono.toPosMulMono`, `MulLeftMono.toPosMulMono`, `posMulMono_iff_posMulStrictMono`, `posMulMono_iff_posMulReflectLT`
`PosMulReflectLE` 📖	CompData	11 math math: `PosMulReflectLT.toPosMulReflectLE`, `WithBot.instPosMulReflectLE`, `MulLeftStrictMono.toPosMulReflectLE`, `posMulReflectLE_iff_posMulReflectLT`, `posMulStrictMono_iff_posMulReflectLE`, `posMulReflectLE_iff_mulPosReflectLE`, `FractionalIdeal.instPosMulReflectLEIdealOfIsDedekindDomain`, `posMulReflectLE_iff`, `PosMulStrictMono.toPosMulReflectLE`, `RCLike.instPosMulReflectLE`, `FractionalIdeal.instPosMulReflectLENonZeroDivisors`
`PosMulReflectLT` 📖	CompData	11 math math: `RCLike.toPosMulReflectLT`, `posMulReflectLT_iff_contravariant_pos`, `posMulReflectLT_iff`, `posMulReflectLE_iff_posMulReflectLT`, `PosMulMono.toPosMulReflectLT`, `posMulReflectLT_iff_mulPosReflectLT`, `MulLeftMono.toPosMulReflectLT`, `WithBot.instPosMulReflectLT`, `posMulMono_iff_posMulReflectLT`, `PosMulReflectLE.toPosMulReflectLT`, `EReal.instPosMulReflectLT`
`PosMulStrictMono` 📖	CompData	17 math math: `WithBot.instPosMulStrictMono`, `ConditionallyCompleteLinearOrderedField.toPosMulStrictMono`, `instPosMulStrictMonoIdeal`, `Ordinal.instPosMulStrictMono`, `posMulStrictMono_iff_mulPosStrictMono`, `posMulStrictMono_iff`, `posMulStrictMono_iff_posMulReflectLE`, `FractionalIdeal.instPosMulStrictMonoNonZeroDivisors`, `MulLeftStrictMono.toPosMulStrictMono`, `PosMulReflectLE.toPosMulStrictMono`, `PosMulReflectLT.toPosMulStrictMono`, `posMulMono_iff_posMulStrictMono`, `PosMulMono.toPosMulStrictMono`, `instPosMulStrictMonoWithZeroOfMulLeftStrictMono`, `IsStrictOrderedRing.toPosMulStrictMono`, `Function.Injective.posMulStrictMono`, `LinearOrderedCommMonoidWithZero.toPosMulStrictMono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_mul_of_le_mul_of_nonneg_left` 📖	—	`Preorder.toLE`	—	—	`LE.le.trans` `mul_le_mul_of_nonneg_left`
`le_mul_of_le_mul_of_nonneg_right` 📖	—	`Preorder.toLE`	—	—	`LE.le.trans` `mul_le_mul_of_nonneg_right`
`le_of_mul_le_mul_left` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`ContravariantClass.elim` `PosMulReflectLE.toContravariantClass`
`le_of_mul_le_mul_of_pos_left` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`le_of_mul_le_mul_left`
`le_of_mul_le_mul_of_pos_right` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`le_of_mul_le_mul_right`
`le_of_mul_le_mul_right` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`ContravariantClass.elim` `MulPosReflectLE.toContravariantClass`
`lt_mul_of_lt_mul_of_nonneg_left` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`LT.lt.trans_le` `mul_le_mul_of_nonneg_left`
`lt_mul_of_lt_mul_of_nonneg_right` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`LT.lt.trans_le` `mul_le_mul_of_nonneg_right`
`lt_of_mul_lt_mul_left` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`ContravariantClass.elim` `PosMulReflectLT.toContravariantClass`
`lt_of_mul_lt_mul_of_nonneg_left` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`lt_of_mul_lt_mul_left`
`lt_of_mul_lt_mul_of_nonneg_right` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`lt_of_mul_lt_mul_right`
`lt_of_mul_lt_mul_right` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`ContravariantClass.elim` `MulPosReflectLT.toContravariantClass`
`mulPosMono_iff` 📖	mathematical	—	`MulPosMono` `Preorder.toLE`	—	—
`mulPosMono_iff_mulPosReflectLT` 📖	mathematical	—	`MulPosMono` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `MulPosReflectLT`	—	`MulPosMono.toMulPosReflectLT` `MulPosReflectLT.toMulPosMono`
`mulPosReflectLE_iff` 📖	mathematical	—	`MulPosReflectLE` `ContravariantClass` `Preorder.toLT` `Preorder.toLE`	—	—
`mulPosReflectLT_iff` 📖	mathematical	—	`MulPosReflectLT` `ContravariantClass` `Preorder.toLE` `Preorder.toLT`	—	—
`mulPosStrictMono_iff` 📖	mathematical	—	`MulPosStrictMono` `Preorder.toLT`	—	—
`mulPosStrictMono_iff_mulPosReflectLE` 📖	mathematical	—	`MulPosStrictMono` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `MulPosReflectLE`	—	`MulPosStrictMono.toMulPosReflectLE` `MulPosReflectLE.toMulPosStrictMono`
`mul_le_mul` 📖	—	`Preorder.toLE`	—	—	`mul_le_mul_of_nonneg'`
`mul_le_mul_iff_left₀` 📖	mathematical	`Preorder.toLT`	`Preorder.toLE`	—	`rel_iff_cov` `MulPosMono.to_covariantClass_pos_mul_le` `MulPosReflectLE.toContravariantClass`
`mul_le_mul_iff_of_pos_left` 📖	mathematical	`Preorder.toLT`	`Preorder.toLE`	—	`mul_le_mul_iff_right₀`
`mul_le_mul_iff_of_pos_right` 📖	mathematical	`Preorder.toLT`	`Preorder.toLE`	—	`mul_le_mul_iff_left₀`
`mul_le_mul_iff_right₀` 📖	mathematical	`Preorder.toLT`	`Preorder.toLE`	—	`rel_iff_cov` `PosMulMono.to_covariantClass_pos_mul_le` `PosMulReflectLE.toContravariantClass`
`mul_le_mul_of_nonneg` 📖	—	`Preorder.toLE`	—	—	`LE.le.trans` `mul_le_mul_of_nonneg_left` `mul_le_mul_of_nonneg_right`
`mul_le_mul_of_nonneg'` 📖	—	`Preorder.toLE`	—	—	`LE.le.trans` `mul_le_mul_of_nonneg_right` `mul_le_mul_of_nonneg_left`
`mul_le_mul_of_nonneg_left` 📖	—	`Preorder.toLE`	—	—	`PosMulMono.mul_le_mul_of_nonneg_left`
`mul_le_mul_of_nonneg_right` 📖	—	`Preorder.toLE`	—	—	`MulPosMono.mul_le_mul_of_nonneg_right`
`mul_le_of_mul_le_of_nonneg_left` 📖	—	`Preorder.toLE`	—	—	`LE.le.trans` `mul_le_mul_of_nonneg_left`
`mul_le_of_mul_le_of_nonneg_right` 📖	—	`Preorder.toLE`	—	—	`LE.le.trans` `mul_le_mul_of_nonneg_right`
`mul_lt_mul` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`mul_lt_mul_of_pos_of_nonneg'`
`mul_lt_mul'` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`mul_lt_mul_of_nonneg_of_pos'`
`mul_lt_mul_iff_left₀` 📖	—	`Preorder.toLT`	—	—	`lt_of_mul_lt_mul_right` `LT.lt.le` `mul_lt_mul_of_pos_right`
`mul_lt_mul_iff_of_pos_left` 📖	—	`Preorder.toLT`	—	—	`mul_lt_mul_iff_right₀`
`mul_lt_mul_iff_of_pos_right` 📖	—	`Preorder.toLT`	—	—	`mul_lt_mul_iff_left₀`
`mul_lt_mul_iff_right₀` 📖	—	`Preorder.toLT`	—	—	`lt_of_mul_lt_mul_left` `LT.lt.le` `mul_lt_mul_of_pos_left`
`mul_lt_mul_of_le_of_lt_of_nonneg_of_pos` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`LE.le.trans_lt` `mul_le_mul_of_nonneg_right` `mul_lt_mul_of_pos_left`
`mul_lt_mul_of_le_of_lt_of_pos_of_nonneg` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`LT.lt.trans_le` `mul_lt_mul_of_pos_left` `mul_le_mul_of_nonneg_right`
`mul_lt_mul_of_lt_of_le_of_nonneg_of_pos` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`LE.le.trans_lt` `mul_le_mul_of_nonneg_left` `mul_lt_mul_of_pos_right`
`mul_lt_mul_of_lt_of_le_of_pos_of_nonneg` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`LT.lt.trans_le` `mul_lt_mul_of_pos_right` `mul_le_mul_of_nonneg_left`
`mul_lt_mul_of_nonneg_of_pos` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`mul_lt_mul_of_lt_of_le_of_nonneg_of_pos`
`mul_lt_mul_of_nonneg_of_pos'` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`mul_lt_mul_of_le_of_lt_of_nonneg_of_pos`
`mul_lt_mul_of_pos` 📖	—	`Preorder.toLT`	—	—	`LT.lt.trans` `mul_lt_mul_of_pos_left` `mul_lt_mul_of_pos_right`
`mul_lt_mul_of_pos'` 📖	—	`Preorder.toLT`	—	—	`LT.lt.trans` `mul_lt_mul_of_pos_right` `mul_lt_mul_of_pos_left`
`mul_lt_mul_of_pos_left` 📖	—	`Preorder.toLT`	—	—	`PosMulStrictMono.mul_lt_mul_of_pos_left`
`mul_lt_mul_of_pos_of_nonneg` 📖	—	`Preorder.toLE` `Preorder.toLT`	—	—	`mul_lt_mul_of_le_of_lt_of_pos_of_nonneg`
`mul_lt_mul_of_pos_of_nonneg'` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`mul_lt_mul_of_lt_of_le_of_pos_of_nonneg`
`mul_lt_mul_of_pos_right` 📖	—	`Preorder.toLT`	—	—	`MulPosStrictMono.mul_lt_mul_of_pos_right`
`mul_lt_of_mul_lt_of_nonneg_left` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`LE.le.trans_lt` `mul_le_mul_of_nonneg_left`
`mul_lt_of_mul_lt_of_nonneg_right` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`LE.le.trans_lt` `mul_le_mul_of_nonneg_right`
`posMulMono_iff` 📖	mathematical	—	`PosMulMono` `Preorder.toLE`	—	—
`posMulMono_iff_mulPosMono` 📖	mathematical	—	`PosMulMono` `MulPosMono`	—	—
`posMulMono_iff_posMulReflectLT` 📖	mathematical	—	`PosMulMono` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `PosMulReflectLT`	—	`PosMulMono.toPosMulReflectLT` `PosMulReflectLT.toPosMulMono`
`posMulReflectLE_iff` 📖	mathematical	—	`PosMulReflectLE` `ContravariantClass` `Preorder.toLT` `Preorder.toLE`	—	—
`posMulReflectLE_iff_mulPosReflectLE` 📖	mathematical	—	`PosMulReflectLE` `MulPosReflectLE`	—	—
`posMulReflectLT_iff` 📖	mathematical	—	`PosMulReflectLT` `ContravariantClass` `Preorder.toLE` `Preorder.toLT`	—	—
`posMulReflectLT_iff_mulPosReflectLT` 📖	mathematical	—	`PosMulReflectLT` `MulPosReflectLT`	—	—
`posMulStrictMono_iff` 📖	mathematical	—	`PosMulStrictMono` `Preorder.toLT`	—	—
`posMulStrictMono_iff_mulPosStrictMono` 📖	mathematical	—	`PosMulStrictMono` `MulPosStrictMono`	—	—
`posMulStrictMono_iff_posMulReflectLE` 📖	mathematical	—	`PosMulStrictMono` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `PosMulReflectLE`	—	`PosMulStrictMono.toPosMulReflectLE` `PosMulReflectLE.toPosMulStrictMono`

---

← Back to Index