Theorems · Theorem · order theory
mul_lt_mul_of_pos_left
∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulStrictMono α],
b < c → 0 < a → a * b < a * c- Defined in
- Mathlib.Algebra.Order.GroupWithZero.Defs
- Cited by
- 71 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.
- Preorderstatement and proof · cited by 7,952
- PosMulStrictMonostatement and proof · cited by 151
- PosMulStrictMono.mul_lt_mul_of_pos_leftproof · cited by 1
Cited by71
Results whose statement or proof uses this declaration.
- Ordinal.isNormal_opowproof · cited by 37
- mul_lt_mul_iff_right₀proof · cited by 14
- mul_neg_of_pos_of_negproof · cited by 13
- ContinuousLinearMap.isOpenMapproof · cited by 6
- mul_lt_mul_of_le_of_lt_of_nonneg_of_posproof · cited by 5
- mul_lt_mul_of_neg_leftproof · cited by 5
- Real.rpow_lt_rpow_of_exponent_ltproof · cited by 5
- pow_right_strictAnti₀proof · cited by 5
- ONote.fundamentalSequence_has_propproof · cited by 5
- lt_mul_of_one_lt_rightproof · cited by 5
- multipliable_one_add_of_summableproof · cited by 4
- NumberField.hermiteTheorem.rank_le_rankOfDiscrBddproof · cited by 4