proposition: Lemma Cint_cycTIiso_coprime x : coprime #[x] a -> sigma w x \in Cint.
proof: Proof. move=> co_x_a; apply: Cint_rat_Aint (Aint_vchar _ Zsigw). have [Qb galQb [QbC AutQbC [w_b genQb memQb]]] := group_num_field_exists <[x]>. have{memQb} [wx Dwx]: exists wx, sigma w x = QbC wx. have /memQb Qbx := dvdnn #[x]. have [sw1 /Qbx[wx1 Dwx1] [sw2 /Qbx[wx2 Dwx2] ->]] := vcharP _ Zsigw. by exists (wx1 - wx2); rewrite rmorphB !cfunE Dwx1 Dwx2. suffices: wx \in fixedField 'Gal({:Qb} / 1). rewrite Dwx (galois_fixedField galQb) ?subvf // => /vlineP[z ->]. by rewrite -in_algE fmorph_eq_rat fmorph_rat Crat_rat. apply/fixedFieldP=> [|v_b _]; first exact: memvf. have [v Dv] := AutQbC v_b; apply: (fmorph_inj QbC); rewrite Dv -Dwx. have [u uQb uQb'] := dvd_restrict_cfAut (W / cfker w) #[x] v. transitivity (sigma (cfAut u w) x); first by rewrite -cfAut_cycTIiso cfunE -uQb. congr (sigma _ _); apply/cfun_inP=> y Wy; rewrite cfunE/= -cfQuoEker //. rewrite uQb' ?char_vchar ?cfQuo_char ?irr_char // coprime_sym. apply: coprime_dvdr co_x_a; rewrite [a]cforder_lin_char //. by rewrite dvdn_exponent ?mem_quotient. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg matrix poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor center gproduct cyclic pgroup abelian frobenius) mathcomp(mxalgebra mxrepresentation vector falgebra fieldext galois) mathcomp(ssrnum rat algC algnum classfun character) mathcomp(integral_char inertia vcharacter) odd_order(PFsection1 PFsection2)