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