Theorems · Theorem · order theory

mul_lt_mul_right_of_neg

∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R] {a b c : R}, c < 0 → (a * c < b * c ↔ b < a)

Defined in

Mathlib.Algebra.Order.Ring.Unbundled.Basic

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

SemiringLinearOrderExistsAddOfLEMulPosStrictMonoAddRightStrictMonoAddRightReflectLT