Theorems · Inductive type · order theory
IsOrderedCancelMonoid
(α : Type u_2) → [CommMonoid α] → [Preorder α] → Prop
An ordered cancellative monoid is an ordered monoid in which multiplication is cancellative and monotone.
- Defined in
- Mathlib.Algebra.Order.Monoid.Defs
- Cited by
- 65 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CommMonoidPreorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement · cited by 7,952
- CommMonoidstatement · cited by 2,264
Cited by69
Results whose statement or proof uses this declaration.
- Finset.mulAntidiagonalstatement and proof · cited by 8
- Finset.prod_lt_prod'statement and proof · cited by 6
- Finset.prod_lt_prod_of_nonempty'statement and proof · cited by 3
- Filter.Tendsto.atTop_of_isBoundedUnder_le_mulstatement and proof · cited by 3
- Filter.Tendsto.atTop_of_mul_isBoundedUnder_lestatement and proof · cited by 3
- Submonoid.closure_image_isMulIndecomposable_baseOfstatement and proof · cited by 2
- Set.IsPWO.mulstatement and proof · cited by 2
- Submonoid.fg_of_divisivestatement and proof · cited by 2
- Filter.Tendsto.atTop_of_const_mulstatement and proof · cited by 2
- Filter.Tendsto.atTop_of_mul_conststatement and proof · cited by 2
- Finset.one_lt_prod'statement and proof · cited by 2
- Multiset.prod_lt_prod'statement and proof · cited by 2