
Vector
Spaces
Title: 
Vector Spaces 
Author:

Holden Lee (holdenl /at/ princeton /dot/ edu)

Submission date: 
20140829 
Abstract: 
This formalisation of basic linear algebra is based completely on locales, building off HOLAlgebra. 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 finitedimensional; vector spaces, definition of dimension; the ranknullity theorem. Some concepts are actually defined and proved for modules as they also apply there. Infinitedimensional vector spaces are supported, but dimension is only supported for finitedimensional vector spaces. The proofs are standard; the proofs of the replacement theorem and ranknullity theorem roughly follow the presentation in Linear Algebra by Friedberg, Insel, and Spence. The ranknullity 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{VectorSpaceAFP,
author = {Holden Lee},
title = {Vector Spaces},
journal = {Archive of Formal Proofs},
month = aug,
year = 2014,
note = {\url{https://isaafp.org/entries/VectorSpace.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Used by: 
Deep_Learning, Isabelle_Marries_Dirac 
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.

