Mathlib Map

Theorems · Theorem · order theory

div_lt_div_of_pos_left

∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b c : G₀}, 0 < a → 0 < c → c < b → a / b < a / c
Defined in
Mathlib.Algebra.Order.GroupWithZero.Basic
Cited by
2 results in Mathlib
Foundations
Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
GroupWithZeroPartialOrderPosMulReflectLTMulPosReflectLT
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

div_lt_self · cited by 3div_lt_selfBehrend.exp_neg_two_mul_le · cited by 1Behrend.exp_neg_two_mul_lePartialOrder · cited by 6410PartialOrderGroupWithZero · cited by 691GroupWithZeroLT.lt.trans · cited by 370lt.transPosMulReflectLT · cited by 278PosMulReflectLTMulPosReflectLT · cited by 93MulPosReflectLTdiv_lt_div_iff_of_pos_left · cited by 3div_lt_div_iff_of_pos_leftdiv_lt_div_of_pos_leftCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.