Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Octonions


view this post on Zulip Email Gateway (Aug 22 2022 at 18:31):

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