Theorems · Inductive type · order theory

IsOrderedModule

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

An ordered module is a module with a partial order such that scalar multiplication by a nonnegative scalar and of a nonnegative vector are both monotone.

Defined in

Mathlib.Algebra.Order.Module.Defs

Cited by

156 results in Mathlib

Foundations

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

Assumes

SMulPreorderPreorderZeroZero