Theorems · Inductive type · order theory

PosSMulReflectLE

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

Typeclass for reverse monotonicity of scalar multiplication by positive elements on the left, namely a • b₁ ≤ a • b₂ → b₁ ≤ 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

51 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

SMulPreorderPreorderZero