Theorems · Theorem · order theory

lt_mul_of_lt_one_left

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

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