Structures · Algebra
CancelCommMonoid
Commutative version of CancelMonoid.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument
Extends2
Extended by1
Forgetful instances
Concrete types that are instances11
- DomMulAct
- Localization
- PNat
- Prod
- OrderDual
- Set.Elem
- ULift
- MulOpposite
- Lex
- Colex
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by35
- Finset.prod_sdiff_eq_prod_sdiff_iff
- eq_iff_eq_of_mul_eq_mul
- isMulFreimanHom_antitone
- Finset.card_Ico_mul_right
- Monoid.exponent_eq_max'_orderOf
- IsMulFreimanHom.mono
- mulRothNumber_map_mul_left
- Function.Injective.cancelCommMonoid
- Pi.cancelCommMonoid
- IsOrderedMonoid.toIsOrderedCancelMonoid'
- ne_iff_ne_of_mul_eq_mul
- ULift.cancelCommMonoid
- IsMulFreimanIso.mono
- Finset.HasMulAntidiagonal.mulAntidiagonal_congr'
- Submonoid.closure_irreducible
- OrderDual.instCancelCommMonoid
- Colex.instCancelCommMonoid
- CancelCommMonoid.toCommMonoid
- CancelCommMonoid.toCancelMonoid
- CancelCommMonoid.toLeftCancelMonoid
- Prod.instCancelCommMonoid
- AffineMonoid.to_twoUniqueProds
- mulRothNumber_map_mul_right
- CancelCommMonoid.toIsLeftCancelMul
- FunLike.cancelCommMonoid
- Lex.instCancelCommMonoid
- DomMulAct.instCancelCommMonoidOfMulOpposite
- Set.MulAntidiagonal.finite_of_isWF
- MulOpposite.instCancelCommMonoid
- Finset.prod_sdiff_ne_prod_sdiff_iff
- Additive.instAddCancelCommMonoid
- card_Ico_one_mul
- Submonoid.LocalizationMap.cancelCommMonoid
- semiconjBy_iff_eq
- Submonoid.LocalizationMap.instCancelCommMonoidLocalization