proposition: Lemma FTtype345_constants : [/\ forall i j, j != 0 -> mu2_ i j 1%g = d%:R, forall j, j != 0 -> delta_ j = delta, (d > 1)%N & n \in Cnat].
proof: Proof. have nz_j1 : #1 != 0 :> Iirr W2 by rewrite Iirr1_neq0. have invj j: j != 0 -> mu2_ 0 j 1%g = d%:R /\ delta_ j = delta. move=> nz_j; have [k co_k_j1 Dj] := cfExp_prime_transitive w2_pr nz_j1 nz_j. rewrite -(cforder_dprodr defW) -dprod_IirrEr in co_k_j1. have{co_k_j1} [[u Dj1u] _] := cycTIiso_aut_exists ctiWM co_k_j1. rewrite dprod_IirrEr -rmorphXn -Dj /= -!dprod_IirrEr -!/(w_ _ _) in Dj1u. rewrite truncCK ?Cnat_irr1 //. have: delta_ j *: mu2_ 0 j == cfAut u (delta_ #1 *: mu2_ 0 #1). by rewrite -!(cycTIiso_prTIirr pddM) -/ctiWM -Dj1u. rewrite raddfZsign /= -prTIirr_aut eq_scaled_irr signr_eq0 /= /mu2_. by case/andP=> /eqP-> /eqP->; rewrite prTIirr_aut cfunE/= aut_Cnat ?Cnat_irr1. have d_gt1: (d > 1)%N. rewrite ltn_neqAle andbC -eqC_nat -ltC_nat truncCK ?Cnat_irr1 //. rewrite irr1_gt0 /= eq_sym; apply: contraNneq nz_j1 => mu2_lin. have: mu2_ 0 #1 \is a linear_char by rewrite qualifE/= irr_char /= mu2_lin. by rewrite lin_irr_der1 => /(prTIirr0P ptiWM)[i /irr_inj/prTIirr_inj[_ ->]]. split=> // [i j /invj[<- _] | _ /invj[//] | ]; first by rewrite prTIirr_1. have: (d%:R == delta %[mod w1])%C by rewrite truncCK ?Cnat_irr1 ?prTIirr1_mod. rewrite /eqCmod unfold_in -/n (negPf (neq0CG W1)) CnatEint => ->. rewrite divr_ge0 ?ler0n // [delta]signrE opprB addrA -natrD subr_ge0 ler1n. by rewrite -(subnKC d_gt1). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum algC classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9)