Cayley-Dickson construction produces a sequence of normed algebras over real numbers. Its consequent applications result in complex numbers, quaternions, octonions, etc. In this paper we formalize the construction and prove its basic properties.
In this article, we formalize in the Mizar system  the notion of the derivative of polynomials over the field of real numbers . To define it, we use the derivative of functions between reals and reals .
The Mazur-Ulam theorem  has been formulated as two registrations: cluster bijective isometric -> midpoints-preserving Function of E, F; and cluster isometric midpoints-preserving -> Affine Function of E, F; A proof given by Jussi Väisälä  has been formalized.