proposition: Lemma leC_norm_invDade chi : '[chi^\rho] <= '[chi] ?= iff (chi == (chi^\rho)^\tau).
proof: Proof. have Achi_rho := invDade_on chi; rewrite -(Dade_isometry ddA) //. set chi1 := _^\tau; rewrite -subr_eq0 -cfnorm_eq0; set mu := chi - chi1. have owv: '[chi1, mu] = 0. by rewrite invDade_reciprocity ?raddfB //= DadeK ?subrr. rewrite -(subrK chi1 chi) -/mu addrC cfnormD owv conjC0 !addr0. split; first by rewrite -subr_ge0 addrC addKr cfnorm_ge0. by rewrite eq_sym addrC -subr_eq0 addrK. Qed.
imports: HB(structures) 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 zmodp) mathcomp(gfunctor gproduct cyclic pgroup commutator nilpotent frobenius) mathcomp(matrix mxalgebra mxrepresentation) odd_order(BGsection3) mathcomp(vector ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection4 PFsection5 PFsection6)