Theorems · Theorem · order theory
smul_nonneg
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
[inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulMono α β], 0 ≤ a → 0 ≤ b₁ → 0 ≤ a • b₁- Defined in
- Mathlib.Algebra.Order.Module.Defs
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
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.
- Preorderstatement and proof · cited by 7,952
- smul_zeroproof · cited by 665
- SMulZeroClassstatement and proof · cited by 213
- PosSMulMonostatement and proof · cited by 188
- smul_le_smul_of_nonneg_leftproof · cited by 47
Cited by21
Results whose statement or proof uses this declaration.
- ConvexOn.smul'proof · cited by 3
- Mathlib.Meta.Positivity.smul_nonneg_of_pos_of_nonnegproof · cited by 3
- ConcaveOn.smul'proof · cited by 3
- slope_nonneg_iff_of_leproof · cited by 3
- CStarAlgebra.span_nonneg_inter_closedBallproof · cited by 2
- smul_nonneg_iffproof · cited by 2
- CFC.abs_smul_nonnegproof · cited by 2
- MeasureTheory.weightedSMul_nonnegproof · cited by 1
- IsStrictlyPositive.smulproof · cited by 1
- MeasureTheory.SimpleFunc.integral_nonnegproof · cited by 1
- MeasureTheory.condExpIndSMul_nonnegproof · cited by 1