fact: Definition algebraicOver (fFtoE : F -> E) u := exists2 p, p != 0 & root (map_poly fFtoE p) u.
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)