Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL | Publicación