Theorems · Theorem · order theory
mul_le_mul_of_nonpos_right
∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b c : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R]
[AddRightReflectLE R], b ≤ a → c ≤ 0 → a * c ≤ b * c- Cited by
- 13 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Preorderstatement and proof · cited by 7,952
- add_zeroproof · cited by 2,707
- zero_addproof · cited by 2,366
- MulZeroClass.mul_zeroproof · cited by 2,091
- add_assocproof · cited by 746
- mul_addproof · cited by 413
- AddRightMonostatement and proof · cited by 367
- ExistsAddOfLEstatement and proof · cited by 330
- mul_le_mul_of_nonneg_rightproof · cited by 301
- Eq.trans_leproof · cited by 155
- MulPosMonostatement and proof · cited by 128
Cited by13
Results whose statement or proof uses this declaration.
- mul_nonneg_of_nonpos_of_nonposproof · cited by 45
- ProbabilityTheory.integrable_exp_mul_of_le_of_leproof · cited by 7
- div_le_iff_of_negproof · cited by 6
- div_le_div_of_nonpos_of_leproof · cited by 4
- antitone_mul_rightproof · cited by 3
- mul_le_mul_of_nonneg_of_nonposproof · cited by 1
- le_mul_of_le_one_leftproof · cited by 1
- mul_le_mul_of_nonpos_of_nonposproof · cited by 1
- sum_trapezoidal_error_adjacent_intervalsproof · cited by 0
- mul_le_mul_of_nonpos_of_nonpos'proof · cited by 0
- mul_le_of_one_le_leftproof · cited by 0
- mul_le_mul_of_nonneg_of_nonpos'proof · cited by 0