proposition: Lemma mapf_root (F : fieldType) (R : ringType) (f : {rmorphism F -> R}) (p : {poly F}) (x : F) : root (p ^^ f) (f x) = root p x.
proof: Proof. by rewrite !rootE horner_map fmorph_eq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)