Structures · Algebra
PosMulMono
Typeclass for monotonicity of multiplication by nonnegative elements on the left,
namely a₁ ≤ a₂ → b * a₁ ≤ b * a₂ if 0 ≤ b.
You should usually not use this very granular typeclass directly, but rather a typeclass like
IsOrderedRing.
- Defined in
- Mathlib.Algebra.Order.GroupWithZero.Defs
- Shape
- One type argument · adds mul_le_mul_of_nonneg_left
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances4
- Rat
- EReal
- WithBot
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by172
- mul_nonneg
- mul_le_mul_of_nonneg_left
- mul_le_mul
- pow_nonneg
- sq_nonneg
- pow_le_pow_left₀
- Finset.prod_le_prod
- Finset.prod_nonneg
- mul_le_mul_iff_right₀
- mul_self_nonneg
- mul_le_of_le_one_right
- pow_le_pow_right₀
- one_le_pow₀
- mul_nonpos_of_nonneg_of_nonpos
- pow_right_mono₀
- one_lt_pow₀
- pow_le_one₀
- le_mul_of_one_le_right
- mul_le_mul_iff_of_pos_left
- pow_le_pow_of_le_one
- mul_lt_mul
- one_le_mul_of_one_le_of_one_le
- mul_le_mul_of_nonpos_left
- mul_max_of_nonneg
- inv_nonpos
- monotone_mul_left_of_nonneg
- inv_neg''
- le_self_pow₀
- Left.mul_nonneg
- div_nonpos_of_nonneg_of_nonpos
- finprod_nonneg
- inv_lt_zero
- finprod_le_finprod
- Multiset.prod_map_le_prod_map₀
- PosMulMono.toPosMulReflectLT
- pow_lt_one₀
- le_mul_iff_one_le_right
- IsSquare.nonneg
- Finset.prod_le_one
- mul_self_le_mul_self
- mul_le_iff_le_one_right
- Multiset.prod_map_nonneg
- Finset.one_le_prod
- mul_lt_one_of_nonneg_of_lt_one_left
- List.prod_map_le_prod_map₀
- pow_left_monotoneOn
- pos_and_pos_or_neg_and_neg_of_mul_pos
- antitone_mul_left
- one_lt_mul_of_lt_of_le
- mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
Ancestors0
No ancestors.