proposition: Lemma eq_in_map_poly_id0 (aR rR : ringType) (f g : aR -> rR) (S : addrClosed aR) : f 0 = 0 -> g 0 = 0 -> {in S, f =1 g} -> {in polyOver S, map_poly f =1 map_poly g}.
proof: Proof. move=> f0 g0 eq_fg p pP; apply/polyP => i. by rewrite !coef_map_id0// eq_fg// (polyOverP _). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)