proposition: Lemma cfExp_prime_transitive G (i j : Iirr G) : prime #|G| -> i != 0 -> j != 0 -> exists2 k, coprime k #['chi_i]%CF & 'chi_j = 'chi_i ^+ k.
proof: Proof. set p := #|G| => pr_p nz_i nz_j; have cycG := prime_cyclic pr_p. have [L [h [injh oL Lh h_ontoL]] [h1 hM hX _ o_h]] := lin_char_group G. rewrite (derG1P (cyclic_abelian cycG)) indexg1 -/p in oL. have /fin_all_exists[h' h'K] := h_ontoL _ (irr_cyclic_lin _ cycG). have o_h' k: k != 0 -> #[h' k] = p. rewrite -cforder_irr_eq1 h'K -o_h => nt_h'k. by apply/prime_nt_dvdP=> //; rewrite cforder_lin_char_dvdG. have{oL} genL k: k != 0 -> generator [set: L] (h' k). move=> /o_h' o_h'k; rewrite /generator eq_sym eqEcard subsetT /=. by rewrite cardsT oL -o_h'k. have [/(_ =P <[_]>)-> gen_j] := (genL i nz_i, genL j nz_j). have /cycleP[k Dj] := cycle_generator gen_j. by rewrite !h'K Dj o_h hX generator_coprime coprime_sym in gen_j *; exists k. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)