Theorems · Definition · order theory
MulLeftMono
(M : Type u_1) → [Mul M] → [LE 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
- 410 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 by415
Results whose statement or proof uses this declaration.
- mul_le_mul'statement and proof · cited by 274
- mul_le_mul_rightstatement and proof · cited by 47
- OrderIso.invstatement and proof · cited by 27
- pow_le_pow_left'statement and proof · cited by 25
- mul_lt_mul_of_lt_of_lestatement and proof · cited by 18
- OrderIso.mulLeftstatement and proof · cited by 18
- le_mul_of_one_le_right'statement and proof · cited by 17
- Finset.prod_le_prod'statement and proof · cited by 17
- mul_le_mul_iff_leftstatement and proof · cited by 15
- mul_right_monostatement and proof · cited by 13
- Finset.prod_le_prod_of_subset_of_one_le'statement and proof · cited by 12
- mabs_of_one_lestatement and proof · cited by 11
Showing the 200 most cited of 415.