proposition: Lemma restr_DadeE : {in 'CF(L, A1), restr_Dade =1 Dade ddA}.
proof: Proof. move=> aa CF1aa; apply/cfunP=> g; rewrite cfunElock. have CFaa: aa \in 'CF(L, A) := cfun_onS sA1A CF1aa. have [a /= /andP[A1a Ha_g] | no_a /=] := pickP. by apply/esym/DadeE; rewrite -1?restr_Dade_support1 ?ssA1A. rewrite cfunElock; case: pickP => //= a /andP[_ Ha_g]. rewrite (cfun_on0 CF1aa) //; apply: contraFN (no_a a) => A1a. by rewrite A1a restr_Dade_support1. 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)