
GaussJordan
Algorithm
and
Its
Applications
Title: 
GaussJordan Algorithm and Its Applications 
Authors:

Jose Divasón and
Jesús Aransay

Submission date: 
20140903 
Abstract: 
The GaussJordan 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 HOLMultivariateAnalysis 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 GaussJordan 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. 
BibTeX: 
@article{Gauss_JordanAFP,
author = {Jose Divasón and Jesús Aransay},
title = {GaussJordan Algorithm and Its Applications},
journal = {Archive of Formal Proofs},
month = sep,
year = 2014,
note = {\url{http://isaafp.org/entries/Gauss_Jordan.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Rank_Nullity_Theorem 
Used by: 
Echelon_Form, Polynomial_Factorization, QR_Decomposition 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

