Theorems · Inductive type · order theory
MulPosMono
(α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
Typeclass for monotonicity of multiplication by nonnegative 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
IsOrderedRing.
- Defined in
- Mathlib.Algebra.Order.GroupWithZero.Defs
- Cited by
- 128 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 by132
Results whose statement or proof uses this declaration.
- mul_le_mul_of_nonneg_rightstatement and proof · cited by 301
- mul_le_mulstatement · cited by 144
- pow_le_pow_left₀statement and proof · cited by 99
- mul_nonneg_of_nonpos_of_nonposstatement and proof · cited by 45
- Finset.prod_le_prodproof · cited by 40
- mul_le_of_le_one_leftstatement and proof · cited by 37
- sq_eq_sq₀statement and proof · cited by 30
- mul_nonpos_of_nonpos_of_nonnegstatement and proof · cited by 24
- le_mul_of_one_le_leftstatement and proof · cited by 19
- mul_le_mul_iff_left₀statement and proof · cited by 19
- mul_lt_mul'statement · cited by 13
- mul_le_mul_of_nonpos_rightstatement and proof · cited by 13