proposition: Lemma cent_mx_ideal m n (R : 'A_(m, n)) : left_mx_ideal 'C(R)%MS 'C(R)%MS.
proof: Proof. apply/mulsmx_subP=> A1 A2 C_A1 C_A2; apply/cent_mxP=> B R_B. by rewrite mulmxA (cent_mxP C_A1) // -!mulmxA (cent_mxP C_A2). 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)