proposition: Lemma dvd_restrict_cfAut a (v : {rmorphism algC -> algC}) : exists2 u : {rmorphism algC -> algC}, forall gT0 G0 chi x, chi \in 'Z[irr (@gval gT0 G0)] -> #[x] %| a -> u (chi x) = v (chi x) & forall chi x, chi \in 'Z[irr G] -> coprime #[x] a -> u (chi x) = chi x.
proof: Proof. have [-> | a_gt0] := posnP a. exists v => // chi x Zchi; rewrite /coprime gcdn0 order_eq1 => /eqP->. by rewrite aut_Cint ?Cint_vchar1. pose b := (#|G|`_(\pi(a)^'))%N. have co_a_b: coprime a b := pnat_coprime (pnat_pi a_gt0) (part_pnat _ _). have [Qa _ [QaC _ [w_a genQa memQa]]] := group_num_field_exists [group of Zp a]. have [Qb _ [QbC _ [w_b genQb memQb]]] := group_num_field_exists [group of Zp b]. rewrite !card_Zp ?part_gt0 // in Qa QaC w_a genQa memQa Qb QbC w_b genQb memQb. have [nu nuQa nuQb] := extend_coprime_Qn_aut QaC QbC v co_a_b genQa genQb. exists nu => [gt0 G0 chi x Zchi x_dv_a | chi x Zchi co_x_a]. without loss{Zchi} Nchi: chi / chi \is a character. move=> IH; case/vcharP: Zchi => [chi1 Nchi1 [chi2 Nchi2 ->]]. by rewrite !cfunE !rmorphB !IH. by have [xa <-] := memQa _ _ _ Nchi x x_dv_a; rewrite nuQa. without loss{Zchi} Nchi: chi / chi \is a character. move=> IH; case/vcharP: Zchi => [chi1 Nchi1 [chi2 Nchi2 ->]]. by rewrite !cfunE rmorphB !IH. have [Gx | /cfun0->] := boolP (x \in G); last by rewrite rmorph0. have{Gx} x_dv_b: (#[x] %| b)%N. rewrite coprime_sym coprime_pi' // in co_x_a. by rewrite -(part_pnat_id co_x_a) partn_dvd ?order_dvdG. by have [xb <-] := memQb _ _ _ Nchi x x_dv_b; rewrite nuQb. 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)