Structures · Algebra
CommSemigroup
A commutative semigroup is a type with an associative commutative (*).
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds mul_comm
Extends2
Extended by2
Concrete types that are instances31
- Int
- Nat
- Real
- Rat
- SeparationQuotient
- Filter.Germ
- LocallyConstant
- DomMulAct
- DirectLimit
- Zsqrtd
- SetSemiring
- Tropical
- UpperSet
- LowerSet
- RingCon.Quotient
- Complex.UnitDisc
- Con.Quotient
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- MulOpposite
- Fin
- Lex
- AddOpposite
- ContinuousMap
- Shrink
- Colex
- Multiplicative
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by101
- mul_left_comm
- mul_right_comm
- mul_mul_mul_comm
- dvd_mul_left
- dvd_mul_of_dvd_right
- mul_dvd_mul
- Dvd.intro_left
- Dvd.dvd.mul_left
- dvd_of_mul_left_eq
- mul_rotate
- Set.center_eq_univ
- exists_eq_mul_left_of_dvd
- dvd_of_mul_left_dvd
- Subsemigroup.square
- starMulAut
- IsIdempotentElem.mul
- mul_rotate'
- mulMulHom
- IsRegular.of_mul_left
- dvd_iff_exists_eq_mul_left
- MulHom.coprod
- isRegular_mul_iff
- IsSquare.mul
- MulLECancellable.of_mul_left
- min_mul_max
- max_mul_min
- fn_min_mul_fn_max
- Matrix.hadamard_kronecker_hadamard
- fn_max_mul_fn_min
- MulHom.coeFn
- OrderDual.instCommSemigroup
- Set.commSemigroup
- Dvd.elim_left
- Set.centralizer_eq_univ
- Matrix.kronecker_hadamard_kronecker
- Pi.commSemigroup
- CommSemigroup.isCommJordan
- ULift.commSemigroup
- Function.Surjective.commSemigroup
- DirectLimit.instCommSemigroupOfMulHomClass
- covariant_swap_mul_of_covariant_mul
- Additive.addCommSemigroup
- mul_mul_mul_comm'
- mulMulHom_apply
- CommSemigroup.toCommMagma
- IsSMulRegular.mul_iff
- Equiv.commSemigroup
- SeparationQuotient.instCommSemigroup
- Set.union_mul_inter_subset
- WithOne.instCommMonoid