Theorems · Theorem · order theory
max_mul_of_nonneg
∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {c : R} [MulPosMono R] (a b : R),
0 ≤ c → max a b * c = max (a * c) (b * c)- Cited by
- 7 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- LinearOrderstatement and proof · cited by 8,572
- MulPosMonostatement and proof · cited by 128
- Monotone.map_maxproof · cited by 55
- monotone_mul_right_of_nonnegproof · cited by 4
Cited by7
Results whose statement or proof uses this declaration.
- Asymptotics.bound_of_isBigO_cofiniteproof · cited by 2
- LinearMap.norm_mkContinuous₂_auxproof · cited by 1
- NNReal.sup_mulproof · cited by 1
- Frullani.tendsto_integral_inv_smul_nhdsWithinproof · cited by 1
- ContinuousLinearMap.opNorm_prodproof · cited by 1
- Polynomial.isNonarchimedean_gaussNormproof · cited by 0