Theorems · Definition · order theory
MulRightMono
(M : Type u_1) → [Mul M] → [LE M] → Prop
Typeclass for monotonicity of multiplication on the right,
namely a₁ ≤ a₂ → a₁ * b ≤ a₂ * b.
You should usually not use this very granular typeclass directly, but rather a typeclass like
IsOrderedMonoid.
- Cited by
- 263 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 11 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.swapproof · cited by 216
- CovariantClassproof · cited by 25
Cited by267
Results whose statement or proof uses this declaration.
- mul_le_mul'statement and proof · cited by 274
- mul_le_mul_leftstatement and proof · cited by 31
- OrderIso.invstatement and proof · cited by 27
- pow_le_pow_left'statement and proof · cited by 25
- mul_le_mul_iff_rightstatement and proof · cited by 19
- le_mul_of_one_le_left'statement and proof · cited by 15
- mul_lt_mul_of_le_of_ltstatement and proof · cited by 15
- OrderIso.mulRightstatement and proof · cited by 14
- tsub_mulstatement and proof · cited by 14
- one_le_mabsstatement and proof · cited by 11
- inv_le_inv_iffstatement and proof · cited by 11
- mul_left_monostatement and proof · cited by 10
Showing the 200 most cited of 267.