Structures · Algebra
Semigroup
A semigroup is a type with an associative (*).
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds mul_assoc
Extends1
Extended by5
Forgetful instances
Every Semigroup is also a
Concrete types that are instances34
- Int
- Nat
- Real
- Rat
- SeparationQuotient
- Filter.Germ
- WithConv
- LocallyConstant
- DomMulAct
- DirectLimit
- Zsqrtd
- ContMDiffMap
- SetSemiring
- Tropical
- Representation.IntertwiningMap
- PEmpty
- RingCon.Quotient
- SubMulAction
- Con.Quotient
- FreeSemigroup
- Magma.AssocQuotient
- Semigrp.carrier
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- Shrink
- Colex
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by262
- mul_assoc
- Dvd.dvd.trans
- dvd_mul_right
- dvd_trans
- map_dvd
- mul_dvd_mul_left
- Dvd.intro
- dvd_mul_of_dvd_left
- dvd_add
- dvd_neg
- Dvd.dvd.mul_right
- IsPrimal
- RightDvd
- dvd_of_mul_right_eq
- Semigroup.mem_center_iff
- Set.centralizer_univ
- Subsemigroup.centralizer
- Commute.left_comm
- Semigrp.of
- FreeSemigroup.lift
- Commute.mul_mul_mul_comm
- Semigrp.ofHom
- Set.centralizer_eq_top_iff_subset
- IsRightRegular.of_mul
- exists_dvd_and_dvd_of_dvd_mul
- Subsemigroup.mem_center_iff
- IsLeftRegular.of_mul
- SemiconjBy.mul_left
- Dvd.dvd.neg_right
- Commute.mul_right
- Subsemigroup.corner
- SemiconjBy.mul_right
- IsLeftRegular.mul
- dvd_of_mul_right_dvd
- Commute.mul_left
- Subsemigroup.topologicalClosure
- mul_sSup_distrib
- Magma.AssocQuotient.lift
- sSup_mul_distrib
- Dvd.elim
- Commute.right_comm
- Dvd.dvd.add
- Hindman.FP.tail
- npowRecAuto
- comp_mul_right
- comp_mul_left
- MulHom.noncommCoprod
- leftCoset_assoc
- Hindman.FP.head
- map_dvd_iff