proposition: Lemma map_resultant (aR rR : ringType) (f : {rmorphism {poly aR} -> rR}) p q : f (lead_coef p) != 0 -> f (lead_coef q) != 0 -> f (resultant p q)= resultant (map_poly f p) (map_poly f q).
proof: Proof. move=> nz_fp nz_fq; rewrite /resultant /Sylvester_mx !size_map_poly_id0 //. rewrite -det_map_mx /= map_col_mx; congr (\det (col_mx _ _)); by apply: map_lin1_mx => v; rewrite map_poly_rV rmorphM /= map_rVpoly. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)