From 9abb88060e5bb6405e603dcbe499794e3e181040 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sun, 31 Mar 2024 18:57:17 +0200
Subject: Possible_Bug

In File test.tex line 51 could not be proven, error massage is in the new file error.txt
---
 .gitignore             |  1 +
 Error.txt              |  0
 latex/stdlib.tex       |  1 +
 library/everything.tex |  1 +
 library/test.tex       | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++
 5 files changed, 57 insertions(+)
 create mode 100644 Error.txt
 create mode 100644 library/test.tex

diff --git a/.gitignore b/.gitignore
index 28ce583..ddb98c3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -41,3 +41,4 @@ premseldump/
 haddocks/
 stack.yaml.lock
 zf*.svg
+Anmerkungen.txt
diff --git a/Error.txt b/Error.txt
new file mode 100644
index 0000000..e69de29
diff --git a/latex/stdlib.tex b/latex/stdlib.tex
index 3673801..4921363 100644
--- a/latex/stdlib.tex
+++ b/latex/stdlib.tex
@@ -43,4 +43,5 @@
     \input{../library/topology/topological-space.tex}
     \input{../library/topology/basis.tex}
     \input{../library/topology/disconnection.tex}
+    \input{../library/test.tex}
 \end{document}
diff --git a/library/everything.tex b/library/everything.tex
index 9b85f83..599bc27 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -26,6 +26,7 @@
 \import{topology/basis.tex}
 \import{topology/disconnection.tex}
 \import{topology/separation.tex}
+\import{test.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
diff --git a/library/test.tex b/library/test.tex
new file mode 100644
index 0000000..d30bbba
--- /dev/null
+++ b/library/test.tex
@@ -0,0 +1,54 @@
+\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