diff options
Diffstat (limited to 'library/algebra/magma.tex')
| -rw-r--r-- | library/algebra/magma.tex | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/library/algebra/magma.tex b/library/algebra/magma.tex index d05ce29..3937b56 100644 --- a/library/algebra/magma.tex +++ b/library/algebra/magma.tex @@ -71,10 +71,13 @@ Let $A$ be a unital magma. Then $\mul(\neutral,\neutral) = \neutral$. \end{proposition} +\begin{proof} + Follows by \cref{unitalmagma_type,unitalmagma_left}. +\end{proof} \begin{proposition}\label{unitalmagma_neutral_unique} Let $A$ be a unital magma. - Let $e$ be a set such that $e\in A$ and for all $x\in A$ we have $\mul(x, e) = x = \mul(e, x)$. + Let $e$ be a set such that $e\in \carrier[A]$ and for all $x\in \carrier[A]$ we have $\mul(x, e) = x = \mul(e, x)$. Then $e = \neutral$. \end{proposition} \begin{proof} @@ -97,5 +100,5 @@ \begin{proof} We have $x\cdot e\in \LeftOrb{e}{A}$ by \cref{left_orbit}. Thus $x\cdot e\in\LeftOrb{f}{A}$ by assumption. - Take $y\in\carrier[A]$ such that $x\cdot e = y\cdot f$ by \cref{left_orbit}. + Take $y$ such that $y\in\carrier[A]$ and $x\cdot e = y\cdot f$ by \cref{left_orbit}. \end{proof} |