Structures · Algebra
LeftCancelSemigroup
A LeftCancelSemigroup is a semigroup such that a * b = a * c implies b = 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 by17
- Equiv.dvd
- Prod.instLeftCancelSemigroup
- ULift.leftCancelSemigroup
- Filter.Germ.instLeftCancelSemigroup
- LeftCancelSemigroup.toSemigroup
- DomMulAct.instLeftCancelSemigroupOfMulOpposite
- Additive.addLeftCancelSemigroup
- Equiv.dvd_apply
- AddOpposite.instLeftCancelSemigroup
- Colex.instLeftCancelSemigroup
- Function.Injective.leftCancelSemigroup
- OrderDual.instLeftCancelSemigroup
- LeftCancelSemigroup.toIsLeftCancelMul
- FunLike.leftCancelSemigroup
- MulOpposite.instRightCancelSemigroup
- Lex.instLeftCancelSemigroup
- Pi.leftCancelSemigroup