proposition: Theorem coprime_degree_support_cfcenter g : coprime (Num.trunc ('chi_i 1%g)) #|g ^: G| -> g \notin ('Z('chi_i))%CF -> 'chi_i g = 0.
proof: Proof. set m := Num.trunc _ => co_m_gG notZg. have [Gg | /cfun0-> //] := boolP (g \in G). have Dm: 'chi_i 1%g = m%:R by rewrite truncK ?Cnat_irr1. have m_gt0: (0 < m)%N by rewrite -ltC_nat -Dm irr1_gt0. have nz_m: m%:R != 0 :> algC by rewrite pnatr_eq0 -lt0n. pose alpha := 'chi_i g / m%:R. have a_lt1: `|alpha| < 1. rewrite normrM normfV normr_nat -{2}(divff nz_m). rewrite lt_def (can_eq (mulfVK nz_m)) eq_sym -{1}Dm -irr_cfcenterE // notZg. by rewrite ler_pM2r ?invr_gt0 ?ltr0n // -Dm char1_ge_norm ?irr_char. have Za: alpha \in Aint. have [u _ /dvdnP[v eq_uv]] := Bezoutl #|g ^: G| m_gt0. suffices ->: alpha = v%:R * 'chi_i g - u%:R * (alpha * #|g ^: G|%:R). rewrite rpredB // rpredM ?rpred_nat ?Aint_irr //. by rewrite mulrC mulrA -Dm Aint_class_div_irr1. rewrite -mulrCA -[v%:R](mulfK nz_m) -!natrM -eq_uv (eqnP co_m_gG). by rewrite mulrAC -mulrA -/alpha mulr_natl mulr_natr mulrS addrK. have [Qn galQn [QnC gQnC [_ _ Qn_g]]] := group_num_field_exists <[g]>. have{Qn_g} [a Da]: exists a, QnC a = alpha. rewrite /alpha; have [a <-] := Qn_g _ G _ (irr_char i) g (dvdnn _). by exists (a / m%:R); rewrite fmorph_div rmorph_nat. have Za_nu nu: sval (gQnC nu) alpha \in Aint by rewrite Aint_aut. have norm_a_nu nu: `|sval (gQnC nu) alpha| <= 1. move: {nu}(sval _) => nu; rewrite fmorph_div rmorph_nat normrM normfV. rewrite normr_nat -Dm -(ler_pM2r (irr1_gt0 (aut_Iirr nu i))) mul1r. congr (_ <= _): (char1_ge_norm g (irr_char (aut_Iirr nu i))). by rewrite !aut_IirrE !cfunE Dm rmorph_nat divfK. pose beta := QnC (galNorm 1 {:Qn} a). have Dbeta: beta = \prod_(nu in 'Gal({:Qn} / 1)) sval (gQnC nu) alpha. rewrite /beta rmorph_prod. apply: eq_bigr => nu _. by case: (gQnC nu) => f /= ->; rewrite Da. have Zbeta: beta \in Num.int. apply: Cint_rat_Aint; last by rewrite Dbeta rpred_prod. rewrite /beta; have /vlineP[/= c ->] := mem_galNorm galQn (memvf a). by rewrite alg_num_field fmorph_rat rpred_rat. have [|nz_a] := boolP (alpha == 0). by rewrite (can2_eq (divfK _) (mulfK _)) // mul0r => /eqP. have: beta != 0 by rewrite Dbeta; apply/prodf_neq0 => nu _; rewrite fmorph_eq0. move/(norm_intr_ge1 Zbeta); rewrite lt_geF //; apply: le_lt_trans a_lt1. rewrite -[`|alpha|]mulr1 Dbeta (bigD1 1%g) ?group1 //= -Da. case: (gQnC _) => /= _ <-. rewrite gal_id normrM -subr_ge0 -mulrBr mulr_ge0 // Da subr_ge0. elim/big_rec: _ => [|nu c _]; first by rewrite normr1 lexx. apply: le_trans; rewrite -subr_ge0 -{1}[`|c|]mul1r normrM -mulrBl. by rewrite mulr_ge0 // subr_ge0 norm_a_nu. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient action countalg finalg zmodp) mathcomp(commutator cyclic center pgroup sylow gseries) mathcomp(nilpotent abelian ssrnum ssrint archimedean polydiv) mathcomp(rat matrix mxalgebra intdiv mxpoly vector falgebra) mathcomp(fieldext separable galois algC cyclotomic algnum) mathcomp(mxrepresentation classfun character)