Email Gateway (Aug 19 2022 at 15:40): Email Gateway (Aug 19 2022 at 15:40):From: Tobias Nipkow <nipkow@in.tum.de>
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).
http://afp.sourceforge.net/entries/VectorSpace.shtml
Last updated: Apr 19 2024 at 12:27 UTC