proposition: Lemma prDade_sub_TIirr i j k : j != 0 -> k != 0 -> mu2_ i j 1%g = mu2_ i k 1%g -> tau (mu2_ i j - mu2_ i k) = delta_ j *: (eta_ i j - eta_ i k).
proof: Proof. move=> nz_j nz_k eq_mu2jk_1. have [-> | k'j] := eqVneq j k; first by rewrite !subrr !raddf0. have [[Itau Ztau] [_ Zsigma]] := (Dade_Zisometry ddA0, cycTI_Zisometry ctiWL). set dmu2 := mu2_ i j - _; set dsw := _ - _; have Dmu2 := prTIirr_id ptiWL. have Zmu2: dmu2 \in 'Z[irr L, A0]. by rewrite zchar_split rpredB ?irr_vchar ?prDade_sub_TIirr_on. apply: eq_signed_sub_cTIiso => // [||x Vx]. - exact: zcharW (Ztau _ Zmu2). - rewrite Itau // cfnormBd ?cfnorm_irr // (cfdot_prTIirr ptiWL). by rewrite (negPf k'j) andbF. have V2x: x \in W :\: W2 by rewrite (subsetP _ x Vx) // setDS ?subsetUr. rewrite !(cfunE, Dade_id) ?(cycTIiso_restrict _ _ Vx) //; last first. by rewrite defA0 inE orbC mem_class_support. by rewrite !Dmu2 // (prDade_TIsign_eq eq_mu2jk_1) !cfunE -mulrBr. 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)