diff options
Diffstat (limited to 'library/algebra/quasigroup.tex')
| -rw-r--r-- | library/algebra/quasigroup.tex | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/library/algebra/quasigroup.tex b/library/algebra/quasigroup.tex index 747ab03..50d7b0f 100644 --- a/library/algebra/quasigroup.tex +++ b/library/algebra/quasigroup.tex @@ -10,27 +10,37 @@ \end{enumerate} such that \begin{enumerate} - \item for all $a, b\in A$ we have $\ldiv (a,b)\in A$. - \item for all $a, b\in A$ we have $\rdiv (a,b)\in A$. - \item for all $a,b \in A$ we have $b = \mul(a,\ldiv (a,b))$. - \item for all $a,b \in A$ we have $b = \ldiv(a,\mul (a,b))$. - \item for all $a,b \in A$ we have $b = \mul(\rdiv (b,a),a)$. - \item for all $a,b \in A$ we have $b = \rdiv(\mul (b,a),a)$. + \item\label{quasigroup_ldiv_type} for all $a,b\in\carrier[A]$ we have $\ldiv[A](a,b)\in\carrier[A]$. + \item\label{quasigroup_rdiv_type} for all $a,b\in\carrier[A]$ we have $\rdiv[A](a,b)\in\carrier[A]$. + \item\label{quasigroup_mul_ldiv} for all $a,b\in\carrier[A]$ we have $b = \mul[A](a,\ldiv[A](a,b))$. + \item\label{quasigroup_ldiv_mul} for all $a,b\in\carrier[A]$ we have $b = \ldiv[A](a,\mul[A](a,b))$. + \item\label{quasigroup_rdiv_mul} for all $a,b\in\carrier[A]$ we have $b = \mul[A](\rdiv[A](b,a),a)$. + \item\label{quasigroup_mul_rdiv} for all $a,b\in\carrier[A]$ we have $b = \rdiv[A](\mul[A](b,a),a)$. \end{enumerate} \end{struct} % Cancelling an element on the left. \begin{lemma}\label{quasigroup_cancel_left} Let $A$ be a quasigroup. - Let $a,b,c \in A$. - Suppose $\mul(a,b) = \mul(a,c)$. + Let $a,b,c\in\carrier[A]$. + Suppose $\mul[A](a,b) = \mul[A](a,c)$. Then $b = c$. \end{lemma} +\begin{proof} + We have $b=\ldiv[A](a,\mul[A](a,b))$ by \cref{quasigroup_ldiv_mul}. + We have $c=\ldiv[A](a,\mul[A](a,c))$ by \cref{quasigroup_ldiv_mul}. + Follows by assumption. +\end{proof} % Cancelling an element on the right. \begin{lemma}\label{quasigroup_cancel_right} Let $A$ be a quasigroup. - Let $a,b,c \in A$. - Suppose $\mul(a,c) = \mul(b,c)$. + Let $a,b,c\in\carrier[A]$. + Suppose $\mul[A](a,c) = \mul[A](b,c)$. Then $a = b$. \end{lemma} +\begin{proof} + We have $a=\rdiv[A](\mul[A](a,c),c)$ by \cref{quasigroup_mul_rdiv}. + We have $b=\rdiv[A](\mul[A](b,c),c)$ by \cref{quasigroup_mul_rdiv}. + Follows by assumption. +\end{proof} |