# [isabelle] New AFP entry: Vector Spaces

*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] New AFP entry: Vector Spaces
*From*: Tobias Nipkow <nipkow at in.tum.de>
*Date*: Fri, 29 Aug 2014 16:50:39 +0200
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

Vector Spaces
Holden Lee
This formalisation of basic linear algebra is based completely on locales,
building off HOL-Algebra. It includes basic definitions: linear combinations,
span, linear independence; linear transformations; interpretation of function
spaces as vector spaces; the direct sum of vector spaces, sum of subspaces; the
replacement theorem; existence of bases in finite-dimensional; vector spaces,
definition of dimension; the rank-nullity theorem. Some concepts are actually
defined and proved for modules as they also apply there. Infinite-dimensional
vector spaces are supported, but dimension is only supported for
finite-dimensional vector spaces. The proofs are standard; the proofs of the
replacement theorem and rank-nullity theorem roughly follow the presentation in
Linear Algebra by Friedberg, Insel, and Spence. The rank-nullity theorem
generalises the existing development in the Archive of Formal Proof (originally
using type classes, now using a mix of type classes and locales).
http://afp.sourceforge.net/entries/VectorSpace.shtml

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*