proposition: Lemma mxrank0 m n : mxrank (0 : 'M[R]_(m,n)) = 0%N.
proof: Proof. by rewrite /mxrank diag0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path tuple) mathcomp(perm fingroup choice ssralg fintype finfun poly polydiv) mathcomp(bigop matrix zmodp mxalgebra) ssrcomplements dvdring mxstructure similar minor binetcauchy stronglydiscrete coherent