Theorems · Inductive type · order theory
IsOrderedMonoid
(α : Type u_2) → [CommMonoid α] → [Preorder α] → Prop
An ordered monoid is a monoid with a preorder such that multiplication is monotone.
- Defined in
- Mathlib.Algebra.Order.Monoid.Defs
- Cited by
- 577 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · 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 by610
Results whose statement or proof uses this declaration.
- MulArchimedeanClassstatement and proof · cited by 81
- MulArchimedeanClass.mkstatement and proof · cited by 63
- FiniteMulArchimedeanClassstatement and proof · cited by 21
- FiniteMulArchimedeanClass.mkstatement and proof · cited by 14
- LinearOrderedCommGroup.Subgroup.genLTOnestatement and proof · cited by 12
- MulArchimedeanClass.mk_invstatement and proof · cited by 9
- Set.preimage_mul_const_Iiostatement and proof · cited by 9
- Set.preimage_mul_const_Iicstatement and proof · cited by 7
- Set.preimage_mul_const_Ioistatement and proof · cited by 7
- zpow_lt_zpow_iff_rightstatement and proof · cited by 6
- MulArchimedeanClass.mk_eq_mkstatement and proof · cited by 6
- MulArchimedeanClass.subgroupstatement and proof · cited by 6
Showing the 200 most cited of 610.