Structures · Algebra
MulPosStrictMono
Typeclass for strict monotonicity of multiplication by positive elements on the right,
namely a₁ < a₂ → a₁ * b < a₂ * b 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 · adds mul_lt_mul_of_pos_right
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances4
- FractionalIdeal
- WithBot
- WithZero
- Ideal
How is a type an instance?
Loading the hierarchy index…
Assumed by83
- mul_lt_mul_of_pos_right
- mul_pos_of_neg_of_neg
- mul_self_pos
- mul_neg_of_neg_of_pos
- mul_lt_mul_iff_left₀
- mul_lt_mul
- mul_pos_iff
- mul_lt_of_lt_one_left
- mul_lt_mul_of_neg_right
- mul_nonneg_iff
- mul_nonneg_iff_of_pos_right
- strictAnti_mul_right
- lt_mul_of_one_lt_left
- mul_lt_mul_iff_of_pos_right
- mul_pos_iff_of_pos_right
- two_mul_le_add_sq
- mul_lt_iff_lt_one_left
- mul_nonneg_iff_pos_imp_nonneg
- strictMono_mul_right_of_pos
- four_mul_le_sq_add
- lt_mul_iff_one_lt_left
- nonneg_of_mul_nonneg_left
- mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
- mul_nonpos_iff
- lt_mul_left
- mul_lt_mul_of_pos_of_nonneg'
- StrictMono.mul_const
- mul_le_mul_right_of_neg
- two_mul_le_add_of_sq_le_mul
- lt_two_mul_self
- mul_neg_iff
- WithTop.mul_left_strictMono
- mul_nonneg_iff_left_nonneg_of_pos
- add_le_mul
- mul_lt_mul_of_pos'
- add_le_mul_of_left_le_right
- lt_mul_of_lt_one_left
- MulPosStrictMono.mul_lt_mul_of_pos_right
- mul_add_mul_lt_mul_add_mul
- mul_lt_mul_of_lt_of_le_of_pos_of_nonneg
- mul_lt_of_one_lt_left
- nonpos_of_mul_nonneg_right
- nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg
- MulPosStrictMono.toSMulPosStrictMono
- Right.mul_pos
- cmp_mul_neg_right
- sub_mul_sub_neg_iff
- cmp_mul_pos_right
- Filter.TendstoNhdsWithinIoi.mul_const
- Function.Injective.mulPosStrictMono
Ancestors0
No ancestors.