Theorems · Inductive type · order theory
MulPosReflectLT
(α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on
the right, namely a₁ * b < a₂ * b → a₁ < a₂ if 0 ≤ b.
You should usually not use this very granular typeclass directly, but rather a typeclass like
IsStrictOrderedRing.
- Defined in
- Mathlib.Algebra.Order.GroupWithZero.Defs
- Cited by
- 93 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 4 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement · cited by 7,952
Cited by97
Results whose statement or proof uses this declaration.
- div_le_iff₀statement and proof · cited by 97
- div_le_div_of_nonneg_rightstatement and proof · cited by 77
- le_div_iff₀statement and proof · cited by 75
- div_le_div₀statement and proof · cited by 53
- div_lt_iff₀statement and proof · cited by 45
- lt_div_iff₀statement and proof · cited by 44
- div_le_one_of_le₀statement and proof · cited by 31
- inv_anti₀statement and proof · cited by 27
- inv_le_inv₀statement and proof · cited by 23
- div_le_div_iff_of_pos_rightstatement and proof · cited by 20
- inv_lt_inv₀statement and proof · cited by 17
- OrderIso.mulRight₀statement and proof · cited by 16