The Cayley-Dickson construction in ACL2

DOI10.4204/EPTCS.249.2MaRDI QIDQ6591107zbMATH OpenFDO

Authors John Cowles, Ruben A. Gamboa

Publication date 21 August 2024

Full work available at URL https://doi.org/10.4204/EPTCS.249.2

Mathematics Subject Classification ID

Vector spaces, linear dependence, rank, lineability (15A03) Composition algebras (17A75) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Cayley-Dickson construction
• The eight Cayley-Dickson doubling products
• Relaxed linear spaces and a generalization of the Cayley-Dickson process
• Sedenions: Algebra and analysis
• A construction relating Clifford algebras and Cayley–Dickson algebras

This page was built for publication: The Cayley-Dickson construction in ACL2

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6591107)