Structures · Algebra
MulLeftReflectLE
Typeclass for reverse monotonicity of multiplication on the left,
namely a * b₁ ≤ a * b₂ → b₁ ≤ b₂.
You should usually not use this very granular typeclass directly, but rather a typeclass like
IsOrderedCancelMonoid.
- Shape
- One type argument · adds le_of_mul_le_mul_left'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by19
- mul_le_mul_iff_left
- le_of_mul_le_mul_left'
- exists_one_le_mul_of_le
- MulLeftReflectLE.le_of_mul_le_mul_left'
- one_le_of_le_mul_right
- instIsLeftCancelMulOfMulLeftReflectLE
- OrderDual.mulLeftReflectLE
- le_one_of_mul_le_right
- mul_le_iff_le_one_right'
- Contravariant.toLeftCancelSemigroup
- Set.Icc_mul_Icc
- Contravariant.MulLECancellable
- OrderedCommGroup.le_of_mul_le_mul_left
- Set.smul_Icc
- le_iff_exists_one_le_mul
- le_mul_iff_one_le_right'
- mulRightReflectLE_of_mulLeftReflectLE
- MulLeftStrictMono.toPosMulReflectLE
- mulLeftStrictMono_of_mulLeftReflectLE
Ancestors0
No ancestors.