proposition: Lemma restrict_aut_to_num_field (nu : {rmorphism algC -> algC}) : (forall x, exists y, nu (QnC x) = QnC y) -> {nu0 : {lrmorphism Qn -> Qn} | {morph QnC : x / nu0 x >-> nu x}}.
proof: Proof. move=> Qn_nu; pose nu0 x := sval (sig_eqW (Qn_nu x)). have QnC_nu0: {morph QnC : x / nu0 x >-> nu x}. by rewrite /nu0 => x; case: (sig_eqW _). have nu0a : additive nu0. by move=> x y; apply: (fmorph_inj QnC); rewrite !(QnC_nu0, rmorphB). have nu0m : multiplicative nu0. split=> [x y|]; apply: (fmorph_inj QnC); rewrite ?QnC_nu0 ?rmorph1 //. by rewrite !rmorphM /= !QnC_nu0. pose nu0aM := GRing.isAdditive.Build Qn Qn nu0 nu0a. pose nu0mM := GRing.isMultiplicative.Build Qn Qn nu0 nu0m. pose nu0RM : GRing.RMorphism.type _ _ := HB.pack nu0 nu0aM nu0mM. pose nu0lM := GRing.isScalable.Build rat Qn Qn *:%R nu0 (fmorph_numZ nu0RM). pose nu0LRM : {lrmorphism _ -> _} := HB.pack nu0 nu0aM nu0mM nu0lM. by exists nu0LRM. 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)