proposition: Lemma eval_mxvec e m n (A : 'M_(m, n)) : eval_mx e (mxvec A) = mxvec (eval_mx e A).
proof: Proof. by rewrite -{2}[A]mxvecK eval_vec_mx vec_mxK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)