### Abstract

The Gauss-Jordan algorithm states that any matrix over a field can be transformed by means of elementary row operations to a matrix in reduced row echelon form. The formalization is based on the Rank Nullity Theorem entry of the AFP and on the HOL-Multivariate-Analysis session of Isabelle, where matrices are represented as functions over finite types. We have set up the code generator to make this representation executable. In order to improve the performance, a refinement to immutable arrays has been carried out. We have formalized some of the applications of the Gauss-Jordan algorithm. Thanks to this development, the following facts can be computed over matrices whose elements belong to a field: Ranks, Determinants, Inverses, Bases and dimensions and Solutions of systems of linear equations. Code can be exported to SML and Haskell.

### License

BSD License

### Topics

- Computer science/Algorithms/Mathematical

### Session Gauss_Jordan

- Rref
- Code_Set
- Code_Matrix
- Elementary_Operations
- Rank
- Gauss_Jordan
- Linear_Maps
- Gauss_Jordan_PA
- Determinants2
- Inverse
- Bases_Of_Fundamental_Subspaces
- System_Of_Equations
- Code_Z2
- Examples_Gauss_Jordan_Abstract
- IArray_Addenda
- Matrix_To_IArray
- Gauss_Jordan_IArrays
- Gauss_Jordan_PA_IArrays
- Bases_Of_Fundamental_Subspaces_IArrays
- System_Of_Equations_IArrays
- Determinants_IArrays
- Inverse_IArrays
- Examples_Gauss_Jordan_IArrays
- Code_Generation_IArrays
- Code_Generation_IArrays_SML
- Code_Rational
- Code_Generation_IArrays_Haskell

### Depends on

- Rank-Nullity Theorem in Linear Algebra

### Used by

- Verified Algorithms for Solving Markov Decision Processes
- Polynomial Factorization
- Echelon Form
- QR Decomposition

### Auto-related entries

- QR Decomposition
- Hermite Normal Form
- Echelon Form

## Cite

×

Gauss_Jordan-AFP

    @article{Gauss_Jordan-AFP,
      author  = {Jose Divasón and Jesús Aransay},
      title   = {Gauss-Jordan Algorithm and Its Applications},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Gauss_Jordan.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 18, 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 3, 2014 : Isabelle2014