Email Gateway (Aug 22 2022 at 18:28): Email Gateway (Aug 22 2022 at 18:28):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’d like to announce a new AFP entry which is available at:
https://www.isa-afp.org/entries/Quaternions.html
Quaternions
by Lawrence C. Paulson
This theory is inspired by the HOL Light development of quaternions, but follows
its own route. Quaternions are developed coinductively, as in the existing
formalisation of the complex numbers. Quaternions are quickly shown to belong to
the type classes of real normed division algebras and real inner product spaces.
And therefore they inherit a great body of facts involving algebraic laws,
limits, continuity, etc., which must be proved explicitly in the HOL Light
version. The development concludes with the geometric interpretation of the
product of imaginary quaternions.
Enjoy,
René
Last updated: Apr 26 2024 at 08:19 UTC