Structures · Algebra
MulPosMono
Typeclass for monotonicity of multiplication by nonnegative 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
IsOrderedRing.
- Defined in
- Mathlib.Algebra.Order.GroupWithZero.Defs
- Shape
- One type argument · adds mul_le_mul_of_nonneg_right
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances3
- EReal
- WithBot
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by121
- mul_le_mul_of_nonneg_right
- mul_le_mul
- pow_le_pow_left₀
- mul_nonneg_of_nonpos_of_nonpos
- mul_le_of_le_one_left
- sq_eq_sq₀
- mul_nonpos_of_nonpos_of_nonneg
- mul_le_mul_iff_left₀
- le_mul_of_one_le_left
- mul_le_mul_of_nonpos_right
- mul_lt_mul'
- mul_le_mul_iff_of_pos_right
- pow_lt_pow_left₀
- sq_le_sq₀
- mul_lt_mul''
- max_mul_of_nonneg
- pow_left_inj₀
- mul_le_one₀
- mul_self_le_mul_self_iff
- mul_le_iff_le_one_left
- pow_left_strictMonoOn₀
- nonneg_le_nonneg_of_sq_le_sq
- pow_le_pow_iff_left₀
- le_mul_iff_one_le_left
- sq_lt_sq₀
- mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
- mul_self_le_mul_self
- mul_add_mul_le_mul_add_mul
- monotone_mul_right_of_nonneg
- le_of_pow_le_pow_left₀
- antitone_mul_right
- zpow_left_strictMonoOn₀
- pow_lt_pow_iff_left₀
- mul_self_lt_mul_self
- pow_left_monotoneOn
- mul_self_inj
- pos_and_pos_or_neg_and_neg_of_mul_pos
- lt_of_pow_lt_pow_left₀
- mul_le_mul_of_nonneg
- pos_of_mul_neg_left
- lt_of_mul_self_lt_mul_self₀
- Monotone.mul_const
- Left.mul_lt_mul_of_nonneg
- one_lt_mul
- mul_lt_one_of_nonneg_of_lt_one_right
- Filter.isCoboundedUnder_ge_mul_of_nonneg
- IsOrderedModule.of_smul_one_mono
- Right.mul_nonneg
- neg_of_mul_pos_right
- strictMonoOn_mul_self
Ancestors0
No ancestors.