proposition: Lemma cent_mxP m n B (R : 'A_(m, n)) : reflect (forall A, A \in R -> A *m B = B *m A) (B \in 'C(R))%MS.
proof: Proof. apply: (iffP cent_rowP) => cEB => [A sAE | i A]. rewrite -[A]mxvecK -(mulmxKpV sAE); move: (mxvec A *m _) => u. rewrite !mulmx_sum_row !linear_sum mulmx_suml; apply: eq_bigr => i _ /=. by rewrite !linearZ -scalemxAl /= cEB. by rewrite cEB // vec_mxK row_sub. 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)