Structures · Algebra
PosMulReflectLT
Typeclass for strict reverse monotonicity of multiplication by nonnegative 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 instances2
- EReal
- WithBot
How is a type an instance?
Loading the hierarchy index…
Assumed by277
- div_pos
- inv_pos
- inv_pos_of_pos
- div_nonneg
- half_pos
- Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos
- inv_nonneg
- div_le_div₀
- div_lt_one
- half_lt_self
- le_div_iff₀'
- one_half_pos
- div_le_one
- Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg
- div_le_iff₀'
- inv_anti₀
- one_div_pos
- OrderIso.mulLeft₀
- inv_nonneg_of_nonneg
- inv_le_inv₀
- zpow_pos
- inv_lt_one_of_one_lt₀
- div_lt_iff₀'
- one_le_div
- inv_lt_inv₀
- lt_div_iff₀'
- inv_le_one_of_one_le₀
- inv_mul_le_iff₀
- lt_of_mul_lt_mul_left
- mul_lt_mul_iff_right₀
- one_lt_inv₀
- one_lt_div
- inv_mul_lt_iff₀
- one_half_lt_one
- div_le_self
- one_div_nonneg
- div_le_div_iff₀
- inv_lt_zero'
- inv_lt_comm₀
- inv_strictAnti₀
- div_neg_of_neg_of_pos
- one_le_inv₀
- inv_lt_one₀
- inv_le_comm₀
- le_inv_mul_iff₀
- zpow_right_strictMono₀
- mul_pos_iff_of_pos_left
- lt_inv_comm₀
- zpow_le_zpow_iff_right₀
- zpow_nonneg