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
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry