proposition: Lemma Dade_isometry : {in 'CF(L, A) &, isometry Dade}.
proof: Proof. move=> alpha beta CFalpha CFbeta /=. rewrite Dade_reciprocity ?Dade_cfun => // [|a Aa u Hu]; last first. by rewrite (DadeE _ Aa) ?mem_Dade_support1 ?Dade_id. rewrite !(cfdotEl _ CFalpha); congr (_ * _); apply: eq_bigr => x Ax. by rewrite cfResE ?(subsetP sAL) // Dade_id. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius ssrnum) mathcomp(matrix mxalgebra mxrepresentation vector algC classfun character) mathcomp(inertia vcharacter) odd_order(PFsection1)