Theorems · Theorem · order theory
mul_lt_mul_iff_right
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α] [MulRightStrictMono α] [MulRightReflectLT α] (a : α) {b c : α},
b * a < c * a ↔ b < c- Cited by
- 18 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.swapproof · cited by 216
- MulRightStrictMonostatement and proof · cited by 108
- MulRightReflectLTstatement and proof · cited by 10
- rel_iff_covproof · cited by 6
Cited by18
Results whose statement or proof uses this declaration.
- inv_lt_inv_iffproof · cited by 9
- div_lt_iff_lt_mulproof · cited by 5
- lt_div_iff_mul_ltproof · cited by 4
- one_lt_div'proof · cited by 3
- Right.inv_lt_one_iffproof · cited by 2
- mul_inv_lt_inv_mul_iffproof · cited by 2
- lt_mul_inv_iff_mul_ltproof · cited by 1
- div_lt_div_iff_rightproof · cited by 1
- mul_inv_lt_iff_lt_mulproof · cited by 1
- Right.one_lt_inv_iffproof · cited by 1
- inv_mul_lt_one_iff_ltproof · cited by 0
- inv_lt_iff_one_lt_mulproof · cited by 0