Theorems · Inductive type · order theory
PosMulReflectLT
(α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on
the left, namely b * a₁ < b * a₂ → 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
- 278 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 by283
Results whose statement or proof uses this declaration.
- div_posstatement and proof · cited by 337
- inv_posstatement and proof · cited by 124
- inv_pos_of_posstatement and proof · cited by 123
- div_nonnegstatement and proof · cited by 103
- half_posstatement and proof · cited by 83
- Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_posstatement and proof · cited by 58
- inv_nonnegstatement and proof · cited by 56
- div_le_div₀statement and proof · cited by 53
- div_lt_onestatement and proof · cited by 38
- half_lt_selfstatement and proof · cited by 38
- le_div_iff₀'statement and proof · cited by 32
- one_half_posstatement and proof · cited by 31
Showing the 200 most cited of 283.