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 Cited by 4 Authors 2 Divasón, Jose 2 Joosten, Sebastiaan J. C. 2 Thiemann, René 2 Yamada, Akihisa Cited in 1 Serial 1 Journal of Automated Reasoning Cited in 5 Fields 2 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) 1 Number theory (11-XX) 1 Field theory and polynomials (12-XX) 1 Commutative algebra (13-XX) Citations by Year