IsarMathLib 1.19.0: Loops

This release adds a theory file about loops. Loops (the kind we talk about here, not to be confused with for example loop algebras) are algebraic structures that are almost like groups, except that we don’t require the operation to be associative. Wikipedia has a nice picture illustrating dependencies between various algebraic structures between magmas and groups which I copy below:

As the picture shows we get a loop when we take a quasigroup and require that an identity (a neutral element of the operation) exists. It can be shown that that identity is unique in the loop. If we denote the loop identity as , then we can define the left and right inverses of a loop element as the only solutions to the equations and . In a loop these inverses do not have to be the same in general. If the loop operation is associative then we get a group and the left and right inverses unify to become the group inverse.

Advertisement

Tags: formalized mathematics, IsarMathLib releases