Theorems · Inductive type · order theory

PosSMulStrictMono

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

Typeclass for strict monotonicity of scalar multiplication by positive 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

128 results in Mathlib

Foundations

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

Assumes

SMulPreorderPreorderZero