summaryrefslogtreecommitdiff
path: root/library/algebra/monoid.tex
blob: 3249a930e493d3d4894e87a2bc4ce2eb8a79a118 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
\import{algebra/semigroup.tex}
\section{Monoid}\label{form_sec_monoid}

\begin{struct}\label{monoid}
    A monoid $A$ is a semigroup equipped with
    \begin{enumerate}
        \item $\neutral$
    \end{enumerate}
    such that
    \begin{enumerate}
        \item\label{monoid_type} $\neutral[A]\in \carrier[A]$.
        \item\label{monoid_right} for all $a\in \carrier[A]$ we have $\mul[A](a,\neutral[A]) = a$.
        \item\label{monoid_left} for all $a\in \carrier[A]$ we have $\mul[A](\neutral[A], a) = a$.
    \end{enumerate}
\end{struct}

\begin{corollary}\label{monoid_implies_semigroup}
    Let $A$ be a monoid. Then $A$ is a semigroup.
\end{corollary}