Abgabe

Submission of Formalisation

1 files changed, 11 insertions, 1 deletions

diff --git a/library/algebra/group.tex b/library/algebra/group.tex
index a79bd2f..449bacb 100644
--- a/library/algebra/group.tex
+++ b/library/algebra/group.tex
@@ -1,5 +1,5 @@
 \import{algebra/monoid.tex}
-\section{Group}
+\section{Group}\label{form_sec_group}
 
 \begin{struct}\label{group}
     A group $G$ is a monoid such that
@@ -80,3 +80,13 @@
 \begin{definition}\label{group_automorphism}
     Let $f$ be a function. $f$ is a group-automorphism iff $G$ is a group and $\dom{f}=G$ and $\ran{f}=G$. 
 \end{definition}
+
+\begin{definition}\label{trivial_group}
+    $G$ is the trivial group iff $G$ is a group and $\{\neutral[G]\}=G$.
+\end{definition}
+
+\begin{theorem}\label{trivial_implies_abelian}
+    Let $G$ be a group.
+    Suppose $G$ is the trivial group.
+    Then $G$ is an abelian group.
+\end{theorem}