From: Manuel Eberl <eberlm@in.tum.de>
Hello,
after last week's entry on Quaternions, I would like to announce a new
entry on Octonions now. However, if you're hoping for one on Septions or
Sedecions next week, you will unfortunately be disappointed – it turns
out 4 and 8 are the only dimensions for which it works out. Sorry.
The new entry is available at:
https://www.isa-afp.org/entries/Octonions.html
Quaternions
by Angeliki Koutsoukou-Argyraki
We develop the basic theory of Octonions, including various identities
and properties of the octonions and of the octonionic product, a
description of 7D isometries and representations of orthogonal
transformations. To this end we first develop the theory of the vector
cross product in 7 dimensions. The development of the theory of
Octonions is inspired by that of the theory of Quaternions by Lawrence
Paulson. However, we do not work within the type class real_algebra_1
because the octonionic product is not associative.
Enjoy,
Manuel
pEpkey.asc
Last updated: Nov 21 2024 at 12:39 UTC