[isabelle] New AFP entry: Vector Spaces

Vector Spaces
Holden Lee

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).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.