Structures · Algebra
IsOrderedMonoid
An ordered monoid is a monoid with a preorder such that multiplication is monotone.
- Defined in
- Mathlib.Algebra.Order.Monoid.Defs
- Shape
- One type argument · adds mul_le_mul_left, mul_le_mul_right
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances16
- ENNReal
- Filter.Germ
- Units
- MeasureTheory.SimpleFunc
- Associates
- ValuativeRel.ValueGroupWithZero
- MonoidWithZeroHom.ValueGroup₀
- Subtype
- Prod
- OrderDual
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- Multiplicative
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by650
- MulArchimedeanClass
- FiniteMulArchimedeanClass
- LinearOrderedCommGroup.Subgroup.genLTOne
- MulArchimedeanClass.mk_inv
- Set.preimage_mul_const_Iio
- Set.preimage_mul_const_Iic
- Set.preimage_mul_const_Ioi
- zpow_lt_zpow_iff_right
- MulArchimedeanClass.mk_lt_mk
- Set.inv_Iio
- MulArchimedeanClass.subgroup
- MulArchimedeanClass.mk_eq_mk
- hasProd_le
- Set.inv_Ioi
- MulArchimedeanClass.orderHom
- zpow_right_strictMono
- Set.preimage_mul_const_Ici
- LinearOrderedCommGroup.Subgroup.genLTOne_unique
- MulArchimedeanClass.subsemigroup
- Set.inv_Iic
- Set.inv_Ici
- nhds_eq_iInf_mabs_div
- mabs_div_le_iff
- Set.inv_Icc
- LocallyFiniteOrder.orderMonoidHom
- FiniteMulArchimedeanClass.subgroup
- Filter.tendsto_atTop_mul_left_of_le'
- inv_le_inv'
- MulArchimedeanClass.min_le_mk_mul
- GroupCone.oneLE
- IsUpperSet.mul_left
- MulArchimedeanClass.mk_mul_eq_mk_left
- Set.preimage_mul_const_Ioc
- existsUnique_zpow_near_of_one_lt
- Set.preimage_mul_const_Ico
- eq_of_mabs_div_le_one
- MulArchimedeanClass.orderHom_mk
- Filter.Tendsto.atTop_mul_one_eventuallyLE
- mabs_eq_self
- MulArchimedeanClass.mk_left_le_mk_mul
- zpow_left_strictMono
- le_hasProd
- MulArchimedeanClass.lift
- LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete
- continuous_mabs
- Set.preimage_mul_const_Ioo
- MulArchimedeanClass.ballSubgroup
- MulArchimedeanClass.mk_eq_top_iff
- prod_le_hasProd
- Set.preimage_mul_const_Icc
Ancestors0
No ancestors.