proposition: Lemma map_rVpoly (u : 'rV_d) : fp (rVpoly u) = rVpoly u^f.
proof: Proof. apply/polyP=> k; rewrite coef_map !coef_rVpoly. by case: (insub k) => [i|]; rewrite /= ?rmorph0 // mxE. 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)