|
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, Polynomial_Factorization |
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.
|
|