Theorems · Theorem · order theory

mul_lt_of_one_lt_right

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

Variant of lt_mul_of_lt_one_right for a negative instead of positive.

Defined in

Mathlib.Algebra.Order.Ring.Unbundled.Basic

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

SemiringPartialOrderExistsAddOfLEPosMulStrictMonoAddRightStrictMonoAddRightReflectLT