Mathlib Map

Theorems · Theorem · order theory

div_le_div_iff_left

∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] [MulRightMono α] {b c : α} (a : α),
  a / b ≤ a / c ↔ c ≤ b
Defined in
Mathlib.Algebra.Order.Group.Unbundled.Basic
Cited by
1 results in Mathlib
Foundations
Depth 15 from the axioms · uses propext
Assumes
GroupLEMulLeftMonoMulRightMono
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

OrderIso.divLeft · cited by 4OrderIso.divLeftdiv_le_div_left' · cited by 2div_le_div_left'Group · cited by 6238Groupdiv_eq_mul_inv · cited by 715div_eq_mul_invMulLeftMono · cited by 410MulLeftMonoMulRightMono · cited by 263MulRightMonoinv_mul_cancel_left · cited by 88inv_mul_cancel_leftmul_le_mul_iff_left · cited by 15mul_le_mul_iff_leftinv_le_inv_iff · cited by 11inv_le_inv_iffdiv_le_div_iff_leftCITED BYCITES

Cites7

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.