Library ▹ Algebra ▹ Monoids
Definition 2.5.1.  Let M be a set, ∗ : M × M → M be an operation on M, e ∈ M. We define:
(M, ∗, e) forms a monoid  :⇔  (M, ∗) forms a semigroup and e is an identity of [M, ∗]  ⇔  ∗ is associative and e is an identity for ∗
Equivalence.  No proof.
References.
  • https://en.wikipedia.org/wiki/Monoid
  • https://mathworld.wolfram.com/Monoid.html
  • https://proofwiki.org/wiki/Definition:Monoid
  • https://ncatlab.org/nlab/show/monoid
  • https://leanprover-community.github.io/mathlib_docs/algebra/group/basic.html#monoid
[View Source]