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.

### Like this:

Like Loading...

*Related*

Tags: formalized mathematics, IsarMathLib releases

This entry was posted on April 6, 2021 at 3:31 pm and is filed under announcements, IsarMathLib releases. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

April 28, 2021 at 11:27 am |

[…] Just another WordPress.com weblog « IsarMathLib 1.19.0: Loops […]