proposition: Lemma restrict_aut_to_normal_num_field (Qn : splittingFieldType rat) (QnC : {rmorphism Qn -> algC})(nu : {rmorphism algC -> algC}) : {nu0 : {lrmorphism Qn -> Qn} | {morph QnC : x / nu0 x >-> nu x}}.
proof: Proof. apply: restrict_aut_to_num_field => x. case: (splitting_field_normal 1%AS x) => rs /eqP Hrs. have: root (map_poly (nu \o QnC) (minPoly 1%AS x)) (nu (QnC x)). by rewrite fmorph_root root_minPoly. rewrite map_Qnum_poly ?minPolyOver // Hrs. rewrite [map_poly _ _](_:_ = \prod_(y <- map QnC rs) ('X - y%:P)); last first. rewrite big_map rmorph_prod /=; apply: eq_bigr => i _. by rewrite rmorphB /= map_polyX map_polyC. rewrite root_prod_XsubC. by case/mapP => y _ ?; exists y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv ssrnum ssrint archimedean rat) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector intdiv) mathcomp(falgebra fieldext separable galois algC cyclotomic)