Theorems · Inductive type · order theory
MulPosStrictMono
(α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
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
- Cited by
- 94 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 4 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement · cited by 7,952
Cited by103
Results whose statement or proof uses this declaration.
- mul_lt_mul_of_pos_rightstatement and proof · cited by 54
- mul_pos_of_neg_of_negstatement and proof · cited by 40
- mul_self_posstatement and proof · cited by 17
- mul_lt_mul_iff_left₀statement and proof · cited by 13
- mul_neg_of_neg_of_posstatement and proof · cited by 13
- mul_lt_mulstatement · cited by 12
- mul_pos_iffstatement and proof · cited by 8
- mul_lt_of_lt_one_leftstatement and proof · cited by 7
- mul_lt_mul_of_neg_rightstatement and proof · cited by 6
- mul_nonneg_iffstatement and proof · cited by 6
- posMulStrictMono_iff_mulPosStrictMonostatement · cited by 5
- lt_mul_of_one_lt_leftstatement and proof · cited by 5