Formalization of linear space theory in the higher-order logic proving system (Q2375439)

The authors present a standard application of HOL4 to a new domain, linear spaces (i.e., vector spaces). They proved 37 standard properties of vector spaces such as the uniqueness of zero (which is also used as the leading example for the presentation of the work), that multiplying an arbitrary vector by a zero scalar results in the zero vector, or that any scalar multiplied by the zero vector results in the zero vector.