Theorems · Theorem · order theory
mul_lt_mul_iff_left
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α] [MulLeftStrictMono α] [MulLeftReflectLT α] (a : α) {b c : α},
a * b < a * c ↔ b < c- Cited by
- 14 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.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MulLeftStrictMonostatement and proof · cited by 146
- MulLeftReflectLTstatement and proof · cited by 16
- rel_iff_covproof · cited by 6
Cited by14
Results whose statement or proof uses this declaration.
- inv_lt_inv_iffproof · cited by 9
- inv_mul_lt_iff_lt_mulproof · cited by 6
- Left.one_lt_inv_iffproof · cited by 6
- Left.inv_lt_one_iffproof · cited by 5
- lt_inv_mul_iff_mul_ltproof · cited by 2
- Set.pairwise_disjoint_Ioc_mul_zpowproof · cited by 2
- mul_inv_lt_inv_mul_iffproof · cited by 2
- lt_inv_mul_iff_ltproof · cited by 1
- div_lt_div_iff_leftproof · cited by 1
- Set.pairwise_disjoint_Ico_mul_zpowproof · cited by 1
- inv_lt_iff_one_lt_mul'proof · cited by 0
- mul_lt_iff_lt_one_left'proof · cited by 0