Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL

Jesús Aransay, Jose Divasón. Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL. Formal Asp. Comput., 28(6):1005-1026, 2016. [doi]

Authors

Jesús Aransay

This author has not been identified. Look up 'Jesús Aransay' in Google

Jose Divasón

This author has not been identified. Look up 'Jose Divasón' in Google