\import{algebra/magma.tex}

\section{Quasigroups}

\begin{struct}\label{quasigroup}
    A quasigroup $A$ is a magma equipped with
    \begin{enumerate}
        \item $\ldiv$
        \item $\rdiv$
    \end{enumerate}
    such that
    \begin{enumerate}
        \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\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\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}