Theorems · Definition · order theory

MulLECancellable

{α : Type u_1} → [Mul α] → [LE α] → α → Prop

An element a : α is MulLECancellable if x ↦ a * x is order-reflecting. We will make a separate version of many lemmas that require [MulLeftReflectLE α] with MulLECancellable assumptions instead. These lemmas can then be instantiated to specific types, like ENNReal, where we can replace the assumption AddLECancellable x by x ≠ ∞.

Defined in

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Cited by

20 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

MulLE