Theorems · Theorem · order theory
div_lt_div_iff_of_pos_right
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
0 < c → (a / c < b / c ↔ a < b)- Cited by
- 15 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- LT.lt.ne'proof · cited by 1,417
- GroupWithZerostatement and proof · cited by 691
- div_mul_cancel₀proof · cited by 122
- MulPosReflectLTstatement and proof · cited by 93
- div_lt_iff₀proof · cited by 45
Cited by15
Results whose statement or proof uses this declaration.
- ContDiffBump.support_eqproof · cited by 8
- Pell.exists_of_not_isSquareproof · cited by 3
- setOfPred_liouvilleWith_subset_auxproof · cited by 2
- Real.logb_lt_logbproof · cited by 2
- Real.logb_lt_logb_iffproof · cited by 2
- HurwitzZeta.hasSum_int_completedCosZetaproof · cited by 2
- strictConvexOn_rpowproof · cited by 2
- one_add_mul_self_lt_rpow_one_addproof · cited by 2
- Complex.norm_cderiv_ltproof · cited by 1
- HurwitzZeta.hasSum_int_completedHurwitzZetaEvenproof · cited by 1
- BoundedContinuousFunction.tietze_extension_stepproof · cited by 1
- Complex.norm_max_aux₁proof · cited by 1