Theorems · Theorem · order theory

div_mul_le_div_mul_of_div_le_div

∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b c d e : α}
  [IsStrictOrderedRing α], a / b ≤ c / d → 0 ≤ e → a / (b * e) ≤ c / (d * e)

Defined in

Mathlib.Algebra.Order.Field.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemifieldPartialOrderPosMulReflectLTIsStrictOrderedRing