Theorems · Theorem · order theory

StrictMono.div_const

∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α]
  {β : Type u_4} [inst_4 : Preorder β] {f : β → α}, StrictMono f → ∀ {c : α}, 0 < c → StrictMono fun x => f x / c

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

SemifieldPartialOrderPosMulReflectLTIsStrictOrderedRingPreorder