proposition: Lemma complexalg_algebraic : integralRange (@ratr [unitRingType of complexalg]).
proof: Proof. move=> x; suff [p p_monic] : integralOver (real_complex _ \o realalg_of _) x. by rewrite (eq_map_poly (fmorph_eq_rat _)); exists p. by apply: complex_algebraic_trans; apply: realalg_algebraic. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)