From 15deff4df111d86c84d808f1c9cc4e30013287d0 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Thu, 11 Apr 2024 13:37:03 +0200
Subject: 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
---
 library/test.tex | 54 ------------------------------------------------------
 1 file changed, 54 deletions(-)
 delete mode 100644 library/test.tex

(limited to 'library/test.tex')

diff --git a/library/test.tex b/library/test.tex
deleted file mode 100644
index d30bbba..0000000
--- a/library/test.tex
+++ /dev/null
@@ -1,54 +0,0 @@
-\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} %muss hier ein enumerate hin
-        \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}
-
-
-\section{Group}
-
-\begin{struct}\label{group}
-    A group $A$ is a monoid such that
-    \begin{enumerate}
-        \item\label{group_inverse} for all $a \in \carrier[A]$ there exist $b \in \carrier[A]$ such that $\mul[A](a, b) =\neutral[A]$.
-    \end{enumerate} 
-\end{struct}    
-
-\begin{abbreviation}\label{cfourdot}
-    $a\cdot b = \mul(a,b)$.
-\end{abbreviation}
-
-\begin{lemma}\label{neutral_is_idempotent}
-    Let $G$ be a group. $\neutral[G]$ is a idempotent element of $G$.
-\end{lemma}
-
-\begin{proposition}\label{leftinverse_eq_rightinverse}
-    Let $G$ be a group and assume $a \in G$.
-    Then there exist $b\in G$ 
-    such that $a \cdot b = \neutral[G]$ and $b \cdot a = \neutral[G]$.
-\end{proposition}
-\begin{proof}
-    There exist $b \in G$ such that $a \cdot b = \neutral[G]$.
-    There exist $c \in G$ such that $b \cdot c = \neutral[G]$.
-    $a \cdot b = \neutral[G]$.
-    $(a \cdot b) \cdot c = (\neutral[G]) \cdot c$.
-    $(a \cdot b) \cdot c = a \cdot (b \cdot c)$.
-    $a \cdot \neutral[G] = \neutral[G] \cdot c$.
-    $c = c \cdot \neutral[G]$.
-    $c = \neutral[G] \cdot c$.
-    $a \cdot \neutral[G] = c \cdot \neutral[G]$.
-    $a \cdot \neutral[G] = c$ by \cref{monoid_right}.
-    $a = c$ by \cref{monoid_right}.
-    $b \cdot a = b \cdot c$.
-    $b \cdot a = \neutral[G]$.
-\end{proof}
\ No newline at end of file
-- 
cgit v1.2.3