Theorems · Definition · order theory
MulLeftStrictMono
(M : Type u_1) → [Mul M] → [LT M] → Prop
Typeclass for monotonicity of multiplication on the left,
namely b₁ < b₂ → a * b₁ < a * b₂.
You should usually not use this very granular typeclass directly, but rather a typeclass like
IsOrderedMonoid.
- Cited by
- 146 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 10 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.
- CovariantClassproof · cited by 25
Cited by147
Results whose statement or proof uses this declaration.
- mul_lt_mul_rightstatement and proof · cited by 17
- mul_lt_mul_of_le_of_ltstatement and proof · cited by 15
- mul_lt_mul_iff_leftstatement and proof · cited by 14
- inv_lt_inv_iffstatement and proof · cited by 9
- mul_lt_mul_of_lt_of_ltstatement and proof · cited by 9
- mulLeftMono_of_mulLeftStrictMonostatement and proof · cited by 8
- inv_lt'statement and proof · cited by 6
- inv_mul_lt_iff_lt_mulstatement and proof · cited by 6
- Finset.prod_lt_prod'statement and proof · cited by 6
- lt_mul_of_one_lt_right'statement and proof · cited by 6
- Left.one_lt_inv_iffstatement and proof · cited by 6
- one_lt_inv'statement · cited by 5