Octonions

Title:	Octonions
Author:	Angeliki Koutsoukou-Argyraki
Submission date:	2018-09-14
Abstract:	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.
BibTeX:	@article{Octonions-AFP, author = {Angeliki Koutsoukou-Argyraki}, title = {Octonions}, journal = {Archive of Formal Proofs}, month = sep, year = 2018, note = {\url{http://isa-afp.org/entries/Octonions.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.