# Vector Spaces

 Title: Vector Spaces Author: Holden Lee (holdenl /at/ princeton /dot/ edu) Submission date: 2014-08-29 Abstract: 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). BibTeX: @article{VectorSpace-AFP, author = {Holden Lee}, title = {Vector Spaces}, journal = {Archive of Formal Proofs}, month = aug, year = 2014, note = {\url{http://isa-afp.org/entries/VectorSpace.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: Deep_Learning