# 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{https://isa-afp.org/entries/Octonions.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License