1 files changed, 4 insertions, 1 deletions
diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex
index bef3166..ed9d2ff 100644
--- a/library/algebra/monoid.tex
+++ b/library/algebra/monoid.tex
@@ -4,10 +4,13 @@
 \begin{struct}\label{monoid}
     A monoid $A$ is a unital magma such that
     \begin{enumerate}
-        \item\label{monoid_assoc} for all $a, b, c$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$.
+        \item\label{monoid_assoc} for all $a,b,c\in\carrier[A]$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$.
     \end{enumerate}
 \end{struct}
 
 \begin{corollary}\label{monoid_implies_semigroup}
     Let $A$ be a monoid. Then $A$ is a semigroup.
 \end{corollary}
+\begin{proof}
+    Follows by \cref{monoid,unitalmagma,semigroup}.
+\end{proof}