Theorems · Theorem · order theory

mul_le_of_one_le_left

∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R]
  [AddRightReflectLE R], b ≤ 0 → 1 ≤ a → a * b ≤ b

Variant of le_mul_of_one_le_left for b non-positive instead of non-negative.

Defined in

Mathlib.Algebra.Order.Ring.Unbundled.Basic

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

SemiringPreorderExistsAddOfLEMulPosMonoAddRightMonoAddRightReflectLE