proposition: Lemma unitrmxE k (M : 'M[R]_k.+1) : (M \is a GRing.unit) = (M \in unitmx).
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg ssrint ssrnum fintype choice) mathcomp(matrix mxalgebra bigop zmodp perm) dvdring mxstructure stronglydiscrete coherent edr