Structures · Algebra
MulPosReflectLT
Typeclass for strict reverse monotonicity of multiplication by nonnegative 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
- EReal
- WithBot
How is a type an instance?
Loading the hierarchy index…
Assumed by92
- div_le_iff₀
- div_le_div_of_nonneg_right
- le_div_iff₀
- div_le_div₀
- div_lt_iff₀
- lt_div_iff₀
- div_le_one_of_le₀
- inv_anti₀
- inv_le_inv₀
- div_le_div_iff_of_pos_right
- inv_lt_inv₀
- div_lt_div_of_pos_right
- OrderIso.mulRight₀
- div_lt_div_iff_of_pos_right
- mul_lt_mul_iff_left₀
- inv_lt_comm₀
- pos_of_mul_pos_left
- div_le_of_le_mul₀
- inv_strictAnti₀
- mul_inv_le_iff₀
- inv_le_comm₀
- lt_of_mul_lt_mul_right
- lt_inv_comm₀
- mul_inv_lt_iff₀
- le_mul_inv_iff₀
- le_inv_comm₀
- div_le_div_of_nonneg_left
- inv_le_of_inv_le₀
- mul_lt_mul_iff_of_pos_right
- mul_pos_iff_of_pos_right
- div_lt_div_iff_of_pos_left
- div_le_div_iff_of_pos_left
- mul_lt_iff_lt_one_left
- lt_mul_inv_iff₀
- div_le_one₀
- one_le_div₀
- lt_mul_iff_one_lt_left
- Right.inv_pos
- Set.inv_Ioo_0_left
- OrderIso.divRight₀
- mul_inv_le_of_le_mul₀
- Set.preimage_mul_const_Iic₀
- div_lt_div_of_pos_left
- Set.preimage_mul_const_Ioi₀
- Set.preimage_mul_const_Ici₀
- Set.preimage_mul_const_Iio₀
- inv_lt_of_inv_lt₀
- Set.inv_Ioi₀
- Right.inv_nonneg
- inv_le_iff_one_le_mul₀