A quasigroup is an algebraic structure that that one gets after adding (sort of) divsibility to magma. Quasigroups differ from groups in that they are not necessarily associative and they do not have to have the neutral element.
According to Wikipedia there are at least two approaches to defining a quasigroup. One defines a quasigroup as a set with a binary operation, and the other, from universal algebra, defines a quasigroup as having three primitive operations. We will use the first approach.
A quasigroup operation does not have to have the neutral element. The left division is defined
as the only solution to the equation
definition
An operation
definition
An operation that has both left and right division is said to have the Latin square property.
definition
A quasigroup is a set with a binary operation that has the Latin square property.
definition
The uniqueness of the left inverse allows us to define the left division as a function.
The union expression as the value of the function extracts the only element
of the set of solutions of the equation
definition
Similarly the right division is defined as a function on
definition
Left and right divisions are binary operations on
lemma lrdiv_binop:
assumes
We will use multiplicative notation for the quasigroup operation. The right and left division will
be denoted
locale quasigroup0
assumes qgroupassum:
defines
defines
defines
The quasigroup operation is closed on
lemma (in quasigroup0) qg_op_closed:
assumes
A couple of properties of right and left division:
lemma (in quasigroup0) lrdiv_props:
assumes
We can cancel the left element on both sides of an equation.
lemma (in quasigroup0) qg_cancel_left:
assumes
We can cancel the right element on both sides of an equation.
lemma (in quasigroup0) qg_cancel_right:
assumes
Two additional identities for right and left division:
lemma (in quasigroup0) lrdiv_ident:
assumes