Theorems · Inductive type · order theory

PosMulMono

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

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

Defined in

Mathlib.Algebra.Order.GroupWithZero.Defs

Cited by

165 results in Mathlib

Foundations

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

Assumes

MulZeroPreorder