proposition: Lemma algebraic_root_polyXY x y : (let pEx p := (p ^ map_poly FtoE).[x%:P] in exists2 p, pEx p != 0 & root (pEx p) y) -> algebraicOver FtoE x -> algebraicOver FtoE y.
proof: Proof. by case=> p nz_px pxy0 /(root_annihilant nz_px)[r]; exists r; auto. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype tuple finfun bigop fingroup perm div) mathcomp(ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly binomial)