proposition: Lemma prDade_sub_TIirr_on i j k : j != 0 -> k != 0 -> mu2_ i j 1%g = mu2_ i k 1%g -> mu2_ i j - mu2_ i k \in 'CF(L, A0).
proof: Proof. move=> nzj nzk eq_mu1. apply/cfun_onP=> g; rewrite defA0 !inE negb_or !cfunE => /andP[A'g V'g]. have [Lg | L'g] := boolP (g \in L); last by rewrite !cfun0 ?subrr. have{Lg} /bigcupP[_ /rcosetsP[x W1x ->] Kx_g]: g \in cover (rcosets K W1). by rewrite (cover_partition (rcosets_partition_mul W1 K)) (sdprodW defL). have [x1 | ntx] := eqVneq x 1%g. have [-> | ntg] := eqVneq g 1%g; first by rewrite eq_mu1 subrr. have{A'g} A1'g: g \notin 1%g |: A by rewrite !inE negb_or ntg. rewrite x1 mulg1 in Kx_g; rewrite -!(cfResE (mu2_ i _) sKL) ?cfRes_prTIirr //. by rewrite !(cfun_onP (prDade_TIres_on _)) ?subrr. have coKx: coprime #|K| #[x] by rewrite (coprime_dvdr (order_dvdG W1x)). have nKx: x \in 'N(K) by have [_ _ /subsetP->] := sdprodP defL. have [/cover_partition defKx _] := partition_cent_rcoset nKx coKx. have def_cKx: 'C_K[x] = W2 by have [_ _ -> //] := ptiWL; rewrite !inE ntx. move: Kx_g; rewrite -defKx def_cKx cover_imset => /bigcupP[z /(subsetP sKL)Lz]. case/imsetP=> _ /rcosetP[y W2y ->] Dg; rewrite Dg !cfunJ //. have V2yx: (y * x)%g \in W :\: W2. rewrite inE -(dprodWC defW) mem_mulg // andbT groupMl //. by rewrite -[x \in W2]andTb -W1x -in_setI tiW12 inE. rewrite 2?{1}prTIirr_id //. have /set1P->: y \in [1]. rewrite -tiW12 inE W2y andbT; apply: contraR V'g => W1'y. by rewrite Dg imset2_f // !inE negb_or -andbA -in_setD groupMr ?W1'y. rewrite -commute1 (prDade_TIsign_eq eq_mu1) !cfunE -mulrBr. by rewrite !dprod_IirrE !cfDprodE // !lin_char1 // subrr mulr0. 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)