Theorems · Inductive type · order theory

MulPosReflectLE

(α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop

Typeclass for reverse monotonicity of multiplication by positive elements on the right, namely a₁ * b ≤ a₂ * b → a₁ ≤ a₂ if 0 < b. You should usually not use this very granular typeclass directly, but rather a typeclass like IsStrictOrderedRing.

Defined in

Mathlib.Algebra.Order.GroupWithZero.Defs

Cited by

17 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

MulZeroPreorder