Structures · Algebra
MulPosReflectLE
Typeclass for reverse monotonicity of multiplication by positive elements on the right,
namely a₁ * b ≤ a₂ * b → a₁ ≤ a₂ if 0 < b.
You should usually not use this very granular typeclass directly, but rather a typeclass like
IsStrictOrderedRing.
- Defined in
- Mathlib.Algebra.Order.GroupWithZero.Defs
- Shape
- One type argument
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- FractionalIdeal
- WithBot
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- le_of_mul_le_mul_right
- mul_le_mul_iff_left₀
- mul_le_mul_iff_of_pos_right
- mul_le_iff_le_one_left
- le_mul_iff_one_le_left
- one_le_of_le_mul_right₀
- le_of_mul_le_mul_of_pos_right
- MulPosReflectLE.toMulPosStrictMono
- mul_right_cancel_iff_of_pos
- MulPosReflectLE.toContravariantClass
- MulPosReflectLE.toMulPosReflectLT
- MulPosReflectLE.toSMulPosReflectLE
- WithBot.instMulPosReflectLE
- eq_and_eq_of_pos_of_le_of_mul_le_mul