Theorems · Theorem · order theory

CanonicallyOrderedAdd.mul_lt_mul_of_lt_of_lt

∀ {R : Type u} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [PosMulStrictMono R]
  {a b c d : R}, a < b → c < d → a * c < b * d

Defined in

Mathlib.Algebra.Order.Ring.Canonical

Cited by

1 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringPartialOrderCanonicallyOrderedAddPosMulStrictMono