Formalisation of groups and monoids

The test.tex file was deleted and all formalisations of groups and monoids was moved to the fitting document of the library. Some proof steps of the new formalisation were optimized for proof time

1 files changed, 19 insertions, 0 deletions

diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex
new file mode 100644
index 0000000..06fcb50
--- /dev/null
+++ b/library/algebra/monoid.tex
@@ -0,0 +1,19 @@
+\import{algebra/semigroup.tex}
+\section{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}
\ No newline at end of file