Theorems · Inductive type · order theory
IsOrderedAddMonoid
(α : Type u_2) → [AddCommMonoid α] → [Preorder α] → Prop
An ordered (additive) monoid is a monoid with a preorder such that addition is monotone.
- Defined in
- Mathlib.Algebra.Order.Monoid.Defs
- Cited by
- 1,659 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- AddCommMonoidPreorder
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.
- AddCommMonoidstatement · cited by 12,281
- Preorderstatement · cited by 7,952
Cited by1,794
Results whose statement or proof uses this declaration.
- ArchimedeanClassstatement and proof · cited by 247
- neg_neg_of_posstatement and proof · cited by 227
- ArchimedeanClass.mkstatement and proof · cited by 174
- toIocModstatement and proof · cited by 109
- FiniteArchimedeanClassstatement and proof · cited by 100
- toIcoModstatement and proof · cited by 99
- toIocDivstatement and proof · cited by 85
- toIcoDivstatement and proof · cited by 84
- abs_lestatement and proof · cited by 64
- abs_eq_selfstatement and proof · cited by 59
- HahnEmbedding.Seedstatement · cited by 55
- MeasureTheory.integral_nonnegstatement and proof · cited by 52
Showing the 200 most cited of 1,794.