proposition: Lemma extend_coprime_Qn_aut a b (Qa Qb : fieldExtType rat) w_a w_b (QaC : {rmorphism Qa -> algC}) (QbC : {rmorphism Qb -> algC}) (mu : {rmorphism algC -> algC}) : coprime a b -> a.-primitive_root w_a /\ <<1; w_a>>%VS = {:Qa}%VS -> b.-primitive_root w_b /\ <<1; w_b>>%VS = {:Qb}%VS -> {nu : {rmorphism algC -> algC} | forall x, nu (QaC x) = mu (QaC x) & forall y, nu (QbC y) = QbC y}.
proof: Proof. move=> coab [pr_w_a genQa] [pr_w_b genQb]. have [k co_k_a Dmu]: {k | coprime k a & mu (QaC w_a) = QaC (w_a ^+ k)}. have prCw: a.-primitive_root (QaC w_a) by rewrite fmorph_primitive_root. by have [k coka ->] := aut_prim_rootP mu prCw; rewrite -rmorphXn; exists k. pose k1 := chinese a b k 1; have /Qn_aut_exists[nu Dnu]: coprime k1 (a * b). rewrite coprimeMr -!(coprime_modl k1) chinese_modl ?chinese_modr //. by rewrite !coprime_modl co_k_a coprime1n. exists nu => [x | y]. have /Fadjoin_polyP[p Qp ->]: x \in <<1; w_a>>%VS by rewrite genQa memvf. rewrite -!horner_map -!map_poly_comp !map_Qnum_poly // Dmu Dnu -rmorphXn /=. by rewrite -[in LHS](prim_expr_mod pr_w_a) /k1 chinese_modl // prim_expr_mod. by rewrite exprM (prim_expr_order pr_w_a) expr1n rmorph1. have /Fadjoin_polyP[p Qp ->]: y \in <<1; w_b>>%VS by rewrite genQb memvf. rewrite -!horner_map -!map_poly_comp !map_Qnum_poly // Dnu -rmorphXn /=. by rewrite -(prim_expr_mod pr_w_b) chinese_modr // prim_expr_mod. by rewrite mulnC exprM (prim_expr_order pr_w_b) expr1n rmorph1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop prime order ssralg finset fingroup morphism) mathcomp(perm automorphism quotient action zmodp finalg center commutator) mathcomp(poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation) mathcomp(vector falgebra fieldext ssrnum algC rat algnum galois) mathcomp(classfun character inertia integral_char vcharacter)