Vector Spaces

swMATH ID: 28662
Software Authors: Holden Lee
Description: Vector Spaces. 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).
Homepage: https://www.isa-afp.org/entries/VectorSpace.html
Related Software: Berlekamp Zassenhaus; Isabelle/HOL; Sqrt_Babylonian; Archive Formal Proofs; Lifting; Transfer; Locales; Mathematica; Maple; Verified LLL; LLL Factorization; fpLLL; HOL Light; HOL; Isabelle
Cited in: 2 Publications

Citations by Year