Structures · Algebra
RightCancelSemigroup
A RightCancelSemigroup is a semigroup such that a * b = c * b implies a = c.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument
Extends2
Extended by1
Concrete types that are instances10
- Filter.Germ
- DomMulAct
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- Colex
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by16
- mul_rightDvd_mul_iff_left
- Filter.Germ.instRightCancelSemigroup
- FunLike.rightCancelSemigroup
- AddOpposite.instRightCancelSemigroup
- Function.Injective.rightCancelSemigroup
- Pi.rightCancelSemigroup
- RightCancelSemigroup.toIsRightCancelMul
- Additive.addRightCancelSemigroup
- Colex.instRightCancelSemigroup
- Lex.instRightCancelSemigroup
- OrderDual.instRightCancelSemigroup
- DomMulAct.instRightCancelSemigroupOfMulOpposite
- RightCancelSemigroup.toSemigroup
- ULift.rightCancelSemigroup
- Prod.instRightCancelSemigroup
- MulOpposite.instLeftCancelSemigroup