proposition: Lemma eq_in_map_poly (aR rR : ringType) (f g : {additive aR -> rR}) (S : addrClosed aR) : {in S, f =1 g} -> {in polyOver S, map_poly f =1 map_poly g}.
proof: Proof. by move=> /eq_in_map_poly_id0; apply; rewrite //?raddf0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)