Structures · Algebra
CancelMonoid
A monoid in which multiplication is cancellative.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument
Extends2
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances9
- DomMulAct
- FreeMonoid
- Prod
- OrderDual
- Set.Elem
- ULift
- MulOpposite
- Lex
- Colex
How is a type an instance?
Loading the hierarchy index…
Assumed by31
- Finset.HasMulAntidiagonal.mulAntidiagonal_congr
- Finset.Nonempty.card_pow_mono
- Finset.card_le_card_pow
- Finset.Nontrivial.pow
- IsMulTorsionFree.pow_right_injective
- Finset.card_pow_mono
- Finset.HasMulAntidiagonal.mulAntidiagonal_subtype_ext
- OrderDual.instCancelMonoid
- CancelMonoid.toIsRightCancelMul
- Lex.instCancelMonoid
- IsIdempotentElem.iff_eq_one
- ULift.cancelMonoid
- IsMulTorsionFree.pow_right_inj
- Colex.instCancelMonoid
- mul_ne_one'
- CancelMonoid.toRightCancelMonoid
- Set.Nontrivial.pow
- eq_one_of_mul_right'
- CancelMonoid.toLeftCancelMonoid
- Function.Injective.cancelMonoid
- MulOpposite.instCancelMonoid
- instIsCancelSMul
- CancelMonoid.toIsCancelMul
- eq_one_of_mul_left'
- mul_eq_one'
- Prod.instCancelMonoid
- Pi.cancelMonoid
- DomMulAct.instCancelMonoidOfMulOpposite
- MonoidHom.instMonoidHomClassMulHom_2
- Finset.HasMulAntidiagonal.mulAntidiagonal_subtype_ext_iff
- FunLike.cancelMonoid