Theorems · Theorem · order theory
lt_of_mul_lt_mul_left
∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulReflectLT α],
a * b < a * c → 0 ≤ a → b < c- Defined in
- Mathlib.Algebra.Order.GroupWithZero.Defs
- Cited by
- 15 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
- PosMulReflectLTstatement and proof · cited by 278
- ContravariantClass.elimproof · cited by 12
Cited by15
Results whose statement or proof uses this declaration.
- inv_posproof · cited by 124
- mul_lt_mul_iff_right₀proof · cited by 14
- pos_of_mul_pos_rightproof · cited by 6
- strictConvexOn_of_slope_strict_mono_adjacentproof · cited by 5
- Nat.totient_prime_pow_succproof · cited by 4
- Real.one_lt_goldenRatioproof · cited by 2
- SimpleGraph.FarFromTriangleFree.le_card_cliqueFinsetproof · cited by 2
- ClassGroup.exists_mem_finset_approx'proof · cited by 1
- PosMulReflectLT.toPosMulMonoproof · cited by 1
- alternatingGroup.nontrivial_of_three_le_cardproof · cited by 1
- Pell.IsFundamental.mul_inv_x_lt_xproof · cited by 1
- Pell.IsFundamental.mul_inv_x_posproof · cited by 1