proposition: Lemma poly_rV_0 n (p : {poly R}) : p == 0 -> poly_rV p == (0 : 'rV[R]_n).
proof: Proof. by move=> /eqP ->; apply/eqP/rowP => i; rewrite !mxE coef0. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly) ssralg_ext