proposition: Lemma zcharD1_seqInd_Dade A : 1%g \notin A -> {subset S <= 'CF(L, 1%g |: A)} -> 'Z[S, L^#] =i 'Z[S, A].
proof: Proof. move=> notA1 A_S phi; rewrite zcharD1E (zchar_split _ A). apply/andb_id2l=> ZSphi; apply/idP/idP=> [phi10 | /cfun_on0-> //]. rewrite -(setU1K notA1) cfun_onD1 {}phi10 andbT. have{phi ZSphi} [c -> _] := free_span seqInd_free (zchar_span ZSphi). by rewrite big_seq memv_suml // => xi /A_S/memvZ. 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 zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrint) mathcomp(ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4)