proposition: Theorem prTIirr1_mod i j : (mu2_ i j 1%g == delta_ j %[mod w1])%C.
proof: Proof. rewrite -(cfRes1 W1) -['Res _](subrK ('Res (delta_ j *: w_ i j))) cfunE. set phi := _ - _; pose a := '[phi, 1]. have phi_on_1: phi \in 'CF(W1, 1%g). apply/cfun_onP=> g; have [W1g | /cfun0-> //] := boolP (g \in W1). rewrite -(coprime_TIg coW12) inE W1g !cfunE !cfResE //= => W2'g. by rewrite prTIirr_id ?cfunE ?subrr // inE W2'g (subsetP sW1W). have{phi_on_1} ->: phi 1%g = a * w1%:R. rewrite mulrC /a (cfdotEl _ phi_on_1) mulVKf ?neq0CG //. by rewrite big_set1 cfun11 conjC1 mulr1. rewrite cfResE // cfunE lin_char1 // mulr1 eqCmod_addl_mul //. by rewrite Cint_cfdot_vchar ?rpred1 ?rpredB ?cfRes_vchar ?rpredZsign ?irr_vchar. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset fingroup) mathcomp(morphism perm automorphism quotient action gfunctor gproduct) mathcomp(center commutator zmodp cyclic pgroup nilpotent hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC classfun) mathcomp(character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3)