proposition: Lemma cent_mx_ring m n (R : 'A_(m, n)) : n > 0 -> mxring 'C(R)%MS.
proof: Proof. move=> n_gt0; rewrite /mxring cent_mx_ideal; apply/mxring_idP. exists 1%:M; split=> [||A _|A _]; rewrite ?mulmx1 ?mul1mx ?scalar_mx_cent //. by rewrite -mxrank_eq0 mxrank1 -lt0n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)