Structures · Algebra
PosMulStrictMono
Typeclass for strict monotonicity of multiplication by positive 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
IsStrictOrderedRing.
- Defined in
- Mathlib.Algebra.Order.GroupWithZero.Defs
- Shape
- One type argument · adds mul_lt_mul_of_pos_left
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances5
- Ordinal
- FractionalIdeal
- WithBot
- WithZero
- Ideal
How is a type an instance?
Loading the hierarchy index…
Assumed by148
- mul_pos
- pow_pos
- mul_lt_mul_of_pos_left
- sq_eq_sq₀
- Finset.prod_pos
- mul_self_pos
- mul_lt_mul_iff_right₀
- mul_neg_of_pos_of_neg
- mul_lt_mul'
- sq_pos_of_pos
- pow_lt_pow_left₀
- pow_lt_pow_right₀
- sq_le_sq₀
- pow_right_strictMono₀
- mul_lt_mul''
- mul_pos_iff_of_pos_left
- nonneg_of_mul_nonneg_right
- mul_pos_iff
- pow_left_inj₀
- mul_self_le_mul_self_iff
- sq_le_one_iff₀
- pow_left_strictMonoOn₀
- nonneg_le_nonneg_of_sq_le_sq
- pow_le_pow_iff_left₀
- mul_nonneg_iff
- pow_right_strictAnti₀
- pow_le_one_iff_of_nonneg
- sq_lt_sq₀
- lt_mul_of_one_lt_right
- mul_lt_mul_iff_of_pos_left
- zpow_right_inj₀
- strictAnti_mul_left
- mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
- mul_lt_mul_of_neg_left
- pow_eq_one_iff_of_nonneg
- le_of_pow_le_pow_left₀
- Submonoid.pos
- one_lt_sq_iff₀
- pow_lt_pow_iff_left₀
- pow_lt_pow_iff_right_of_lt_one₀
- mul_nonneg_iff_pos_imp_nonneg
- mul_self_lt_mul_self
- sq_lt_one_iff₀
- zpow_eq_one_iff_right₀
- strictMono_mul_left_of_pos
- mul_self_inj
- lt_of_pow_lt_pow_left₀
- pow_lt_one_iff_of_nonneg
- one_le_pow_iff_of_nonneg
- sign_cases_of_C_mul_pow_nonneg
Ancestors0
No ancestors.