(* Title: Octonions.thy Author: Angeliki Koutsoukou-Argyraki, University of Cambridge Date: September 2018 *) section‹Theory of Octonions› theory Octonions imports Cross_Product_7 begin subsection‹Basic definitions› text‹As with the complex numbers, coinduction is convenient.›