proposition: Lemma map_mpoly_comp : injective f -> (p \mPo lq)^f = (p^f) \mPo [tuple of [seq map_mpoly f q | q <- lq]].
proof: Proof. move=> inj_f; apply/mpolyP=> m; rewrite mcoeff_map_mpoly. rewrite !raddf_sum (perm_big _ (msupp_map_mpoly _ inj_f)) /=. apply/eq_bigr=> m' _; rewrite mcoeff_map_mpoly !mcoeffCM rmorphM /=. congr *%R; rewrite /mmap1 -mcoeff_map_mpoly rmorph_prod /=. by congr _@__; apply/eq_bigr=> i /=; rewrite tnth_map rmorphXn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg