Theorems · Theorem · order theory

mul_lt_of_one_lt_left

∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a b : R} [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R], b < 0 → 1 < a → a * b < b

Variant of lt_mul_of_one_lt_left for b negative instead of positive.

Defined in

Mathlib.Algebra.Order.Ring.Unbundled.Basic

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

SemiringPartialOrderExistsAddOfLEMulPosStrictMonoAddRightStrictMonoAddRightReflectLT