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

### License

BSD License

### Topics

- Mathematics/Algebra

### Session VectorSpace

- RingModuleFacts
- FunctionLemmas
- MonoidSums
- LinearCombinations
- SumSpaces
- VectorSpace

### Used by

- Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
- Expressiveness of Deep Learning
- Polynomial Factorization

## Cite

×

VectorSpace-AFP

    @article{VectorSpace-AFP,
      author  = {Holden Lee},
      title   = {Vector Spaces},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/VectorSpace.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Sep 7, 2014 : Isabelle2014
- Aug 31, 2014 : Isabelle2014
- Aug 29, 2014 : Isabelle2014