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.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Used by: Deep_Learning, Jordan_Normal_Form