proposition: Lemma map_prod_XsubC (aR rR : ringType) (f : {rmorphism aR -> rR}) rs : map_poly f (\prod_(x <- rs) ('X - x%:P)) = \prod_(x <- map f rs) ('X - x%:P).
proof: Proof. by rewrite rmorph_prod big_map; apply/eq_bigr => x /=; rewrite map_polyXsubC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)