Structures · Algebra
PosMulReflectLE
Typeclass for reverse monotonicity of multiplication by positive elements on the left,
namely b * a₁ ≤ b * a₂ → 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 instances3
- FractionalIdeal
- WithBot
- Ideal
How is a type an instance?
Loading the hierarchy index…
Assumed by16
- mul_le_mul_iff_right₀
- mul_le_mul_iff_of_pos_left
- le_of_mul_le_mul_left
- le_of_mul_le_mul_of_pos_left
- le_mul_iff_one_le_right
- mul_le_iff_le_one_right
- one_le_of_le_mul_left₀
- PosMulReflectLE.toPosMulStrictMono
- mul_left_cancel_iff_of_pos
- Mathlib.Tactic.FieldSimp.le_eq_cancel_le
- PosMulReflectLE.toMulPosReflectLE
- WithBot.instPosMulReflectLE
- PosMulReflectLE.toPosMulReflectLT
- PosMulReflectLE.toPosSMulReflectLE
- eq_and_eq_of_pos_of_le_of_mul_le_mul
- PosMulReflectLE.toContravariantClass