Theorems · Theorem · order theory
mul_le_mul_of_nonneg
∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α] [MulPosMono α],
a ≤ b → c ≤ d → 0 ≤ a → 0 ≤ d → a * c ≤ b * d- Defined in
- Mathlib.Algebra.Order.GroupWithZero.Defs
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- LE.le.transproof · cited by 3,151
- mul_le_mul_of_nonneg_leftproof · cited by 361
- mul_le_mul_of_nonneg_rightproof · cited by 301
- PosMulMonostatement and proof · cited by 165
- MulPosMonostatement and proof · cited by 128
Cited by3
Results whose statement or proof uses this declaration.
- MvPowerSeries.gaussNorm_add_le_maxproof · cited by 1
- PadicInt.toZModPow_ofIntSeq_of_pow_dvd_subproof · cited by 1
- Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip₀₁'proof · cited by 1