Theorems · Theorem · order theory

smul_le_smul_of_nonneg_left

∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [PosSMulMono α β], b₁ ≤ b₂ → 0 ≤ a → a • b₁ ≤ a • b₂

Defined in

Mathlib.Algebra.Order.Module.Defs

Cited by

47 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

SMulPreorderPreorderZeroPosSMulMono