proposition: Lemma cent_rowP m n B (R : 'A_(m, n)) : reflect (forall i (A := vec_mx (row i R)), A *m B = B *m A) (B \in 'C(R))%MS.
proof: Proof. apply: (iffP sub_kermxP); rewrite mul_vec_lin => cBE. move/(canRL mxvecK): cBE => cBE i A /=; move/(congr1 (row i)): cBE. rewrite row_mul mul_rV_lin -/A; move/(canRL mxvecK). by move/(canRL (subrK _)); rewrite !linear0 add0r. apply: (canLR vec_mxK); apply/row_matrixP=> i. by rewrite row_mul mul_rV_lin /= cBE subrr !linear0. 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)