Theorems · Theorem · order theory
mul_lt_mul
∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α]
[MulPosStrictMono α], a < b → c ≤ d → 0 < c → 0 ≤ b → a * c < b * dAlias of mul_lt_mul_of_pos_of_nonneg'.
Alias of mul_lt_mul_of_lt_of_le_of_pos_of_nonneg.
- Defined in
- Mathlib.Algebra.Order.GroupWithZero.Defs
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 9 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.
- Preorderstatement · cited by 7,952
- PosMulMonostatement · cited by 165
- MulPosStrictMonostatement · cited by 94
- mul_lt_mul_of_pos_of_nonneg'proof · cited by 2
Cited by12
Results whose statement or proof uses this declaration.
- Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_posproof · cited by 6
- EuclideanGeometry.dist_lt_of_angle_ltproof · cited by 1
- ClassGroup.exists_mem_finset_approx'proof · cited by 1
- Pell.d_posproof · cited by 1
- GaussianInt.mod_four_eq_three_of_nat_prime_of_primeproof · cited by 1
- Besicovitch.TauPackage.mem_iUnionUpTo_lastStepproof · cited by 1
- List.prod_map_lt_prod_mapproof · cited by 1
- StrictMonoOn.exists_deriv_lt_slopeproof · cited by 1
- StrictMonoOn.exists_slope_lt_derivproof · cited by 1
- Decidable.mul_lt_mul''proof · cited by 0
- StrictMono.mul_monotoneproof · cited by 0
- div_lt_div₀proof · cited by 0