Structures · Algebra
IsOrderedCancelMonoid
An ordered cancellative monoid is an ordered monoid in which multiplication is cancellative and monotone.
- Defined in
- Mathlib.Algebra.Order.Monoid.Defs
- Shape
- One type argument · adds le_of_mul_le_mul_left, le_of_mul_le_mul_right
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances8
- Filter.Germ
- Localization
- PNat
- Subtype
- Prod
- OrderDual
- Lex
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by87
- Finset.mulAntidiagonal
- Finset.prod_lt_prod'
- Filter.Tendsto.atTop_of_mul_isBoundedUnder_le
- Filter.Tendsto.atTop_of_isBoundedUnder_le_mul
- Finset.prod_lt_prod_of_nonempty'
- Filter.Tendsto.atTop_of_mul_const
- Finset.one_lt_prod'
- Set.IsPWO.mul
- Multiset.prod_lt_prod'
- Filter.Tendsto.atTop_of_const_mul
- Submonoid.closure_image_isMulIndecomposable_baseOf
- Submonoid.fg_of_divisive
- Filter.Tendsto.atTop_of_le_const_mul
- Finset.support_mulAntidiagonal_subset_mul
- one_lt_finprod
- Multiset.prod_lt_prod_of_nonempty'
- exists_pow_lt_of_one_lt
- Finset.prod_lt_prod_of_subset'
- Finset.mem_mulAntidiagonal
- one_lt_finprod_cond
- Set.IsWF.mul
- Finset.prod_lt_one'
- Localization.mkOrderEmbedding
- Filter.Tendsto.atTop_of_mul_le_const
- Localization.mk_le_mk
- Filter.Tendsto.atBot_of_mul_isBoundedUnder_ge
- Finset.single_lt_prod'
- Fintype.prod_strictMono'
- Submonoid.mem_closure_image_one_lt_iff
- Fintype.prod_lt_one_iff_of_le_one
- Pi.Lex.isOrderedCancelMonoid
- OrderDual.isOrderedCancelMonoid
- Finset.isPWO_support_mulAntidiagonal
- exists_lt_pow_of_lt_one
- Localization.partialOrder
- Finset.mulAntidiagonal_mono_left
- Finset.exists_le_of_prod_le'
- Finset.exists_one_lt_of_prod_one_of_exists_ne_one'
- Localization.decidableLT
- Finset.prod_sdiff_lt_prod_sdiff
- threeGPFree_insert_of_lt
- Filter.Germ.instIsOrderedCancelMonoid
- CommMonoid.fg_of_wellQuasiOrderedLE
- IsOrderedCancelMonoid.toIsOrderedMonoid
- Finset.mulAntidiagonal_min_mul_min
- Fintype.prod_lt_one
- Filter.Tendsto.atBot_of_mul_const
- SubmonoidClass.toIsOrderedCancelMonoid
- IsOrderedCancelMonoid.le_of_mul_le_mul_right
- Fintype.one_lt_prod_iff_of_one_le