proposition: Lemma alg_integral (F : fieldType) (L : fieldExtType F) : integralRange (in_alg L).
proof: Proof. move=> x; have [/polyOver1P[p Dp]] := (minPolyOver 1 x, monic_minPoly 1 x). by rewrite Dp map_monic; exists p; rewrite // -Dp root_minPoly. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path tuple bigop finset prime order) mathcomp(ssralg poly polydiv mxpoly countalg closed_field) mathcomp(ssrnum ssrint archimedean rat intdiv fingroup) mathcomp(finalg zmodp cyclic pgroup sylow vector falgebra) mathcomp(fieldext separable galois)