### Abstract

In this contribution, we present some formalizations based on the HOL-Multivariate-Analysis session of Isabelle. Firstly, a generalization of several theorems of such library are presented. Secondly, some definitions and proofs involving Linear Algebra and the four fundamental subspaces of a matrix are shown. Finally, we present a proof of the result known in Linear Algebra as the “Rank-Nullity Theorem”, which states that, given any linear map f from a finite dimensional vector space V to a vector space W, then the dimension of V is equal to the dimension of the kernel of f (which is a subspace of V) and the dimension of the range of f (which is a subspace of W). The proof presented here is based on the one given by Sheldon Axler in his book Linear Algebra Done Right. As a corollary of the previous theorem, and taking advantage of the relationship between linear maps and matrices, we prove that, for every matrix A (which has associated a linear map between finite dimensional vector spaces), the sum of its null space and its column space (which is equal to the range of the linear map) is equal to the number of columns of A.

### License

BSD License

### History

July 14, 2014
  Added some generalizations that allow us to formalize the Rank-Nullity Theorem over finite dimensional vector spaces, instead of over the more particular euclidean spaces. Updated abstract.

### Topics

- Mathematics/Algebra

### Session Rank_Nullity_Theorem

- Dual_Order
- Mod_Type
- Miscellaneous
- Fundamental_Subspaces
- Dim_Formula

### Used by

- Perron-Frobenius Theorem for Spectral Radius Analysis
- Echelon Form
- QR Decomposition
- Gauss-Jordan Algorithm and Its Applications

## Cite

×

Rank_Nullity_Theorem-AFP

    @article{Rank_Nullity_Theorem-AFP,
      author  = {Jose Divasón and Jesús Aransay},
      title   = {Rank-Nullity Theorem in Linear Algebra},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Rank_Nullity_Theorem.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
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- Jan 16, 2013 : Isabelle2012