Theorems · Theorem · order theory

lt_mul_of_lt_one_right

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

Variant of mul_lt_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