Theorems · Inductive type · order theory

PosSMulMono

(α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero α] → Prop

Typeclass for monotonicity of scalar multiplication by nonnegative elements on the left, namely b₁ ≤ b₂ → a • b₁ ≤ a • b₂ if 0 ≤ a. You should usually not use this very granular typeclass directly, but rather a typeclass like IsOrderedModule.

Defined in

Mathlib.Algebra.Order.Module.Defs

Cited by

188 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 4 definitions · uses no axioms

Assumes

SMulPreorderPreorderZero